1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
5 -/
6
7 import linear_algebra.basic linear_algebra.finsupp order.zorn
src └──────────────────┘ └────────────────────┘ └────────┘
8
9 /-!
10
11 # Linear independence and bases
12
13 This file defines linear independence and bases in a module or vector space.
14
15 It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
16
17 ## Main definitions
18
19 All definitions are given for families of vectors, i.e. `v : ι → M` where M is the module or
20 vectorspace and `ι : Type*` is an arbitrary indexing type.
21
22 * `linear_independent R v` states that the elements of the family `v` are linear independent
23
24 * `linear_independent.repr hv x` returns the linear combination representing `x : span R (range v)`
25 on the linear independent vectors `v`, given `hv : linear_independent R v`
26 (using classical choice). `linear_independent.repr hv` is provided as a linear map.
27
28 * `is_basis R v` states that the vector family `v` is a basis, i.e. it is linear independent and
29 spans the entire space
30
31 * `is_basis.repr hv x` is the basis version of `linear_independent.repr hv x`. It returns the
32 linear combination representing `x : M` on a basis `v` of `M` (using classical choice).
33 The argument `hv` must be a proof that `is_basis R v`. `is_basis.repr hv` is given as a linear
34 map as well.
35
36 * `is_basis.constr hv f` constructs a linear map `M₁ →ₗ[R] M₂` given the values `f : ι → M₂` at the
37 basis `v : ι → M₁`, given `hv : is_basis R v`.
38
39 ## Main statements
40
41 * `is_basis.ext` states that two linear maps are equal if they coincide on a basis.
42
43 * `exists_is_basis` states that every vector space has a basis.
44
45 ## Implementation notes
46
47 We use families instead of sets because it allows us to say that two identical vectors are linearly
48 dependent. For bases, this is useful as well because we can easily derive ordered bases by using an
49 ordered index type ι.
50
51 If you want to use sets, use the family `(λ x, x : s → M)` given a set `s : set M`. The lemmas
52 `linear_independent.to_subtype_range` and `linear_independent.of_subtype_range` connect those two
53 worlds.
54
55 ## Tags
56
57 linearly dependent, linear dependence, linearly independent, linear independence, basis
58
59 -/
60
61 noncomputable theory
62
63 open function lattice set submodule
64 open_locale classical
65
66 variables {ι : Type*} {ι' : Type*} {R : Type*} {K : Type*}
67 {M : Type*} {M' : Type*} {V : Type*} {V' : Type*}
68
69 section module
70 variables {v : ι → M}
71 variables [ring R] [add_comm_group M] [add_comm_group M']
id └──┘ ┴└────────────┘ └────────────┘
src └──┘ └────────────┘ └────────────┘
typ └──┘ ┴└────────────┘ └────────────┘
72 variables [module R M] [module R M']
id └────┘ └────┘
src └────┘ └────┘
typ └────┘ └────┘
doc └────┘ └────┘
73 variables {a b : R} {x y : M}
74 include R
75
76 variables (R) (v)
77 /-- Linearly independent family of vectors -/
78 def linear_independent : Prop := (finsupp.total ι M R v).ker = ⊥
id └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
79 variables {R} {v}
80
81 theorem linear_independent_iff : linear_independent R v ↔
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴
doc └────────────────┘
82 ∀l, finsupp.total ι M R v l = 0 → l = 0 :=
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
83 by simp [linear_independent, linear_map.ker_eq_bot']
id └────────────────┘ └────────────────────┘
src └────┘└────────────────┘└┘└────────────────────┘└─
typ └────┘└────────────────┘└┘└────────────────────┘└─
doc └────┘└────────────────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────────────────────
84
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
85 theorem linear_independent_iff' : linear_independent R v ↔
id └────────────────┘ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴
doc └────────────────┘
86 ∀ s : finset ι, ∀ g : ι → R, s.sum (λ i, g i • v i) = 0 → ∀ i ∈ s, g i = 0 :=
id └────┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └──┘ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘
87 linear_independent_iff.trans
id └────────────────────┘└────┘
src └────────────────────┘└────┘
typ └────────────────────┘└────┘
88 ⟨λ hf s g hg i his, have h : _ := hf (s.sum $ λ i, finsupp.single i (g i)) $
id └┘ ┴ ┴ └┘ ┴ └─┘ └┘ ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴
src └──┘ └────────────┘
typ └┘ ┴ ┴ └┘ ┴ └─┘ └┘ ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴
doc └────────────┘
89 by simpa only [linear_map.map_sum, finsupp.total_single] using hg, calc
id └────────────────┘ └──────────────────┘ └┘
src └──────────┘└────────────────┘└┘└──────────────────┘└──────┘
typ └──────────┘└────────────────┘└┘└──────────────────┘└──────┘└┘
doc └──────────┘ └┘ └──────┘
txt └──────────┘ └┘ └──────┘
par └──────────┘ └┘ └──────┘
pid ┴└──┘└┘ └┘ ┴┴└────┘
st └─────────────────────────────────────────────────────────────┘
90 g i = (finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (finsupp.single i (g i)) :
id ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └────────────┘ ┴ ┴ ┴
src └────────────┘ └┘ └─┘ ┴ └────────────┘
typ ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └────────────┘ ┴ ┴ ┴
doc └┘ └────────────┘
91 by rw [finsupp.lapply_apply, finsupp.single_eq_same]
id └──────────────────┘ └────────────────────┘
src └──┘└──────────────────┘└┘└────────────────────┘└─
typ └──┘└──────────────────┘└┘└────────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────────────┘└──────────────────────┘┴└
92 ... = s.sum (λ j, (finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (finsupp.single j (g j))) :
id ┴└──┘ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └────────────┘ ┴ ┴ ┴
src ───┘ └──┘ └────────────┘ └┘ └─┘ ┴ └────────────┘
typ ───┘ ┴└──┘ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └────────────┘ ┴ ┴ ┴
doc ───┘ └┘ └────────────┘
txt ───┘
par ───┘
pid ───┘
st ───┘
93 eq.symm $ finset.sum_eq_single i
id └─────┘ └──────────────────┘ ┴
src └─────┘ └──────────────────┘
typ └─────┘ └──────────────────┘ ┴
94 (λ j hjs hji, by rw [finsupp.lapply_apply, finsupp.single_eq_of_ne hji])
id ┴ └─┘ └─┘ └──────────────────┘ └─────────────────────┘ └─┘
src └──┘└──────────────────┘└┘└─────────────────────┘┴ ┴
typ ┴ └─┘ └─┘ └──┘└──────────────────┘└┘└─────────────────────┘┴└─┘┴
doc └──┘ └┘ ┴ ┴
txt └──┘ └┘ ┴ ┴
par └──┘ └┘ ┴ ┴
pid └┘ └┘ ┴ ┴
st └───────────────────────┘└───────────────────────────┘┴
95 (λ hnis, hnis.elim his)
id └──┘ └──┘└───┘ └─┘
src └───┘
typ └──┘ └──┘└───┘ └─┘
96 ... = s.sum (λ j, finsupp.single j (g j)) i : (finsupp.lapply i : (ι →₀ R) →ₗ[R] R).map_sum.symm
id ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └─────┘ └──┘
src └──┘ └────────────┘ └────────────┘ └┘ └─┘ ┴ └─────┘ └──┘
typ ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ ┴ └─┘┴┴ ┴ └─────┘ └──┘
doc └────────────┘ └┘
97 ... = 0 : finsupp.ext_iff.1 h i,
id └─────────────┘┴ ┴ ┴
src └─────────────┘┴
typ └─────────────┘┴ ┴ ┴
98 λ hf l hl, finsupp.ext $ λ i, classical.by_contradiction $ λ hni, hni $ hf _ _ hl _ $
id └┘ ┴ └┘ └─────────┘ ┴ └────────────────────────┘ └─┘ └─┘ └┘ └┘
src └─────────┘ └────────────────────────┘
typ └┘ ┴ └┘ └─────────┘ ┴ └────────────────────────┘ └─┘ └─┘ └┘ └┘
99 finsupp.mem_support_iff.2 hni⟩
id └─────────────────────┘┴ └─┘
src └─────────────────────┘┴
typ └─────────────────────┘┴ └─┘
100
101 lemma linear_independent_empty_type (h : ¬ nonempty ι) : linear_independent R v :=
id ┴ └──────┘ ┴ └────────────────┘ ┴ ┴
src ┴ └──────┘ └────────────────┘
typ ┴ └──────┘ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘
102 begin
st └─────
103 rw [linear_independent_iff],
id └────────────────────┘
src └──┘└────────────────────┘┴
typ └──┘└────────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────────────────┘└──
104 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ──────┘└─
105 ext i,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ─────┘└─
106 exact false.elim (not_nonempty_iff_imp_false.1 h i)
id └────────┘ └────────────────────────┘ ┴ ┴
src └────┘└────────┘┴ └────────────────────────┘└─┘ ┴ └┘
typ └────┘└────────┘┴ └────────────────────────┘└─┘┴┴┴└┘
doc └────┘ ┴ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └┘
par └────┘ ┴ └─┘ ┴ └┘
pid ┴ ┴ └─┘ ┴ ┴┴
st ────────────────────────────────────────────────────┘
107 end
st └─┘
108
109 lemma ne_zero_of_linear_independent
110 {i : ι} (ne : 0 ≠ (1:R)) (hv : linear_independent R v) : v i ≠ 0 :=
id ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └────────────────┘ ┴
typ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
111 λ h, ne $ eq.symm begin
id ┴ └┘ └─────┘
src └┘ └─────┘
typ ┴ └┘ └─────┘
st └─────
112 suffices : (finsupp.single i 1 : ι →₀ R) i = 0, {simpa},
id └────────────┘ ┴ └┘ ┴ ┴ ┴
src └─────────┘ └────────────┘┴ └───┘ ┴└┘┴ └┘ ┴┴└┘ └───┘
typ └─────────┘ └────────────┘┴ └───┘┴┴└┘┴┴└┘┴┴┴└┘ └───┘
doc └─────────┘ └────────────┘┴ └───┘ ┴└┘┴ └┘ ┴ └┘ └───┘
txt └─────────┘ ┴ └───┘ ┴ ┴ └┘ ┴ └┘ └───┘
par └─────────┘ ┴ └───┘ ┴ ┴ └┘ ┴ └┘ └───┘
pid └───────┘└┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴┴
st ───────────────────────────────────────────────┘└──────┘└┘└
113 rw linear_independent_iff.1 hv (finsupp.single i 1),
id └────────────────────┘ └┘ └────────────┘ ┴
src └─┘└────────────────────┘└─┘ ┴ └────────────┘┴ └─┘
typ └─┘└────────────────────┘└─┘└┘┴ └────────────┘┴┴└─┘
doc └─┘ └─┘ ┴ └────────────┘┴ └─┘
txt └─┘ └─┘ ┴ ┴ └─┘
par └─┘ └─┘ ┴ ┴ └─┘
pid ┴ └─┘ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
114 {simp},
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ──────┘└┘└
115 {simp [h]}
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────┘└─
116 end
st ──┘
117
118 lemma linear_independent.comp
119 (h : linear_independent R v) (f : ι' → ι) (hf : injective f) : linear_independent R (v ∘ f) :=
id └────────────────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ └───────┘ └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────┘
120 begin
st └─────
121 rw [linear_independent_iff, finsupp.total_comp],
id └────────────────────┘ └────────────────┘
src └──┘└────────────────────┘└┘└────────────────┘┴
typ └──┘└────────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────────────┘└──────────────────┘└──
122 intros l hl,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
123 have h_map_domain : ∀ x, (finsupp.map_domain f l) (f x) = 0,
id └────────────────┘ ┴ ┴ ┴
src └──────────────────┘ └┘ ┴ └────────────────┘┴ ┴ └┘ ┴ └┘┴└┘
typ └──────────────────┘ └┘ ┴ └────────────────┘┴ ┴┴└┘ ┴┴ └┘┴└┘
doc └──────────────────┘ └┘ ┴ └────────────────┘┴ ┴ └┘ ┴ └┘ └┘
txt └──────────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
par └──────────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
pid └───────────────┘└─┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴┴
st ────────────────────────────────────────────────────────────┘
124 by rw linear_independent_iff.1 h (finsupp.map_domain f l) hl; simp,
id └────────────────────┘ ┴ └────────────────┘ ┴ ┴ └┘
src └─┘└────────────────────┘└─┘ ┴ └────────────────┘┴ ┴ └┘ └──┘
typ └─┘└────────────────────┘└─┘┴┴ └────────────────┘┴┴┴┴└┘└┘ └──┘
doc └─┘ └─┘ ┴ └────────────────┘┴ ┴ └┘ └──┘
txt └─┘ └─┘ ┴ ┴ ┴ └┘ └──┘
par └─┘ └─┘ ┴ ┴ ┴ └┘ └──┘
pid ┴ └─┘ ┴ ┴ ┴ └┘
st └────────────────────┘ └─
125 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
126 convert h_map_domain a,
id └──────────┘ ┴
src └──────┘ ┴
typ └──────┘└──────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ───────────────────────┘└─
127 simp only [finsupp.map_domain_apply hf],
id └──────────────────────┘ └┘
src └─────────┘└──────────────────────┘┴ ┴
typ └─────────┘└──────────────────────┘┴└┘┴
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid ┴└──┘└┘ ┴ ┴
st ────────────────────────────────────────┘└─
128 end
st ──┘
129
130 lemma linear_independent_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : linear_independent R v :=
id ┴ ┴ └────────────────┘ ┴ ┴
src ┴ └────────────────┘
typ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘
131 linear_independent_iff.2 (λ l hl, finsupp.eq_zero_of_zero_eq_one zero_eq_one _)
id └────────────────────┘┴ ┴ └┘ └────────────────────────────┘ └─────────┘
src └────────────────────┘┴ └────────────────────────────┘
typ └────────────────────┘┴ ┴ └┘ └────────────────────────────┘ └─────────┘
132
133 lemma linear_independent.unique (hv : linear_independent R v) {l₁ l₂ : ι →₀ R} :
id └────────────────┘ ┴ ┴ ┴ └┘ ┴
src └────────────────┘ └┘
typ └────────────────┘ ┴ ┴ ┴ └┘ ┴
doc └────────────────┘ └┘
134 finsupp.total ι M R v l₁ = finsupp.total ι M R v l₂ → l₁ = l₂ :=
id └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘
src └───────────┘ ┴ └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘
doc └───────────┘ └───────────┘
135 by apply linear_map.ker_eq_bot.1 hv
id └───────────────────┘ └┘
src └────┘└───────────────────┘└─┘ └
typ └────┘└───────────────────┘└─┘└┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st └─────────────────────────────────
136
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
137 lemma linear_independent.injective (zero_ne_one : (0 : R) ≠ 1) (hv : linear_independent R v) :
id ┴ ┴ └────────────────┘ ┴ ┴
src ┴ └────────────────┘
typ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘
138 injective v :=
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
139 begin
st └─────
140 intros i j hij,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
141 let l : ι →₀ R := finsupp.single i (1 : R) - finsupp.single j 1,
id ┴ └┘ ┴ ┴ ┴ ┴ └────────────┘ ┴
src └──────┘ ┴└┘┴ └──┘ ┴ ┴ └──┘ └┘┴┴└────────────┘┴ └┘
typ └──────┘┴┴└┘┴┴└──┘ ┴┴┴ └──┘┴└┘┴┴└────────────┘┴┴└┘
doc └──────┘ ┴└┘┴ └──┘ ┴ ┴ └──┘ └┘ ┴└────────────┘┴ └┘
txt └──────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘
par └──────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘
pid └───┘└─┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────┘└─
142 have h_total : finsupp.total ι M R v l = 0,
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘└───────────┘┴ ┴ ┴ ┴ ┴ ┴┴└┘
typ └─────────────┘└───────────┘┴┴┴┴┴┴┴┴┴┴┴┴└┘
doc └─────────────┘└───────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └──────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────────────┘└─
143 { rw finsupp.total_apply,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└────────────────────┘└─
144 rw finsupp.sum_sub_index,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────┘└─
145 { simp [finsupp.sum_single_index, hij] },
id └──────────────────────┘ └─┘
src └────┘└──────────────────────┘└┘ └┘
typ └────┘└──────────────────────┘└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────┘└───────────────────────────────────┘└┘└
146 { intros, apply sub_smul } },
id └──────┘
src └────┘ └────┘└──────┘┴
typ └────┘ └────┘└──────┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴
st ───────────┘└───────────────┘└──┘└
147 have h_single_eq : finsupp.single i (1 : R) = finsupp.single j 1,
id ┴ ┴ └────────────┘ ┴
src └─────────────────┘ ┴ ┴ └──┘ └┘ ┴└────────────┘┴ └┘
typ └─────────────────┘ ┴┴┴ └──┘┴└┘ ┴└────────────┘┴┴└┘
doc └─────────────────┘ ┴ ┴ └──┘ └┘ ┴└────────────┘┴ └┘
txt └─────────────────┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘
par └─────────────────┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘
pid └──────────────┘└─┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────┘└─
148 { rw linear_independent_iff at hv,
id └────────────────────┘
src └─┘└────────────────────┘└────┘
typ └─┘└────────────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ───┘└─────────────────────────────┘└─
149 simp [eq_add_of_sub_eq' (hv l h_total)] },
id └───────────────┘ └┘ ┴ └─────┘
src └────┘└───────────────┘┴ ┴ ┴ └─┘
typ └────┘└───────────────┘┴ └┘┴┴┴└─────┘└─┘
doc └────┘ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ └─┘
pid ┴┴ ┴ ┴ ┴ └┘┴
st ───────────────────────────────────────────┘└┘└
150 show i = j,
id ┴ ┴
src └───┘ ┴ ┴
typ └───┘┴┴ ┴┴
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴
par └───┘ ┴ ┴
pid └───┘ ┴ ┴
st ──────────────
151 { apply or.elim ((finsupp.single_eq_single_iff _ _ _ _).1 h_single_eq),
id └─────┘ └──────────────────────────┘ └─────────┘
src └────┘└─────┘┴ └──────────────────────────┘└──────────┘ ┴
typ └────┘└─────┘┴ └──────────────────────────┘└──────────┘└─────────┘┴
doc └────┘ ┴ └──────────┘ ┴
txt └────┘ ┴ └──────────┘ ┴
par └────┘ ┴ └──────────┘ ┴
pid ┴ ┴ └──────────┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
152 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
153 exact λ h, false.elim (zero_ne_one.symm h.1) }
id └────────┘ └──────────────┘
src └────┘ └──┘└────────┘┴ └──────────────┘┴ └──┘
typ └────┘ └──┘└────────┘┴ └──────────────┘┴ └──┘
doc └────┘ └──┘ ┴ ┴ └──┘
txt └────┘ └──┘ ┴ ┴ └──┘
par └────┘ └──┘ ┴ ┴ └──┘
pid ┴ └──┘ ┴ ┴ └─┘┴
st ────────────────────────────────────────────────┘└─
154 end
st ──┘
155
156 lemma linear_independent_span (hs : linear_independent R v) :
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
doc └────────────────┘
157 @linear_independent ι R (span R (range v))
id └────────────────┘ ┴ ┴ └──┘ ┴ └───┘ ┴
src └────────────────┘ └──┘ └───┘
typ └────────────────┘ ┴ ┴ └──┘ ┴ └───┘ ┴
doc └────────────────┘ └──┘ └───┘
158 (λ i : ι, ⟨v i, subset_span (mem_range_self i)⟩) _ _ _ :=
id ┴ ┴ ┴ └─────────┘ └────────────┘ ┴
src └─────────┘ └────────────┘
typ ┴ ┴ ┴ └─────────┘ └────────────┘ ┴
159 begin
st └─────
160 rw linear_independent_iff at *,
id └────────────────────┘
src └─┘└────────────────────┘└───┘
typ └─┘└────────────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───────────────────────────────┘└─
161 intros l hl,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
162 apply hs l,
id └┘ ┴
src └────┘ ┴
typ └────┘└┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────┘└─
163 have := congr_arg (submodule.subtype (span R (range v))) hl,
id └───────┘ └───────────────┘ └──┘ ┴ └───┘ ┴ └┘
src └──────┘└───────┘┴ └───────────────┘┴ └──┘┴ ┴ └───┘┴ └──┘
typ └──────┘└───────┘┴ └───────────────┘┴ └──┘┴┴┴ └───┘┴┴└──┘└┘
doc └──────┘ ┴ ┴ └──┘┴ ┴ └───┘┴ └──┘
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘
par └──────┘ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────┘└─
164 convert this,
id └──┘
src └──────┘
typ └──────┘└──┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────────┘└─
165 rw [finsupp.total_apply, finsupp.total_apply],
id └─────────────────┘ └─────────────────┘
src └──┘└─────────────────┘└┘└─────────────────┘┴
typ └──┘└─────────────────┘└┘└─────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────┘└───────────────────┘└──
166 unfold finsupp.sum,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └──────────┘
st ───────────────────┘└─
167 rw linear_map.map_sum (submodule.subtype (span R (range v))),
id └────────────────┘ └───────────────┘ └──┘ ┴ └───┘ ┴
src └─┘└────────────────┘┴ └───────────────┘┴ └──┘┴ ┴ └───┘┴ └─┘
typ └─┘└────────────────┘┴ └───────────────┘┴ └──┘┴┴┴ └───┘┴┴└─┘
doc └─┘ ┴ ┴ └──┘┴ ┴ └───┘┴ └─┘
txt └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
par └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────┘└─
168 simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
169 end
st └─┘
170
171 section subtype
172 /- The following lemmas use the subtype defined by a set in M as the index set ι. -/
173
174 theorem linear_independent_comp_subtype {s : set ι} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
175 linear_independent R (v ∘ subtype.val : s → M) ↔
id └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └────────────────┘ ┴ └─────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
doc └────────────────┘
176 ∀ l ∈ (finsupp.supported R R s), (finsupp.total ι M R v) l = 0 → l = 0 :=
id ┴ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ └───────────┘ ┴ ┴
typ ┴ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘
177 begin
st └─────
178 rw [linear_independent_iff, finsupp.total_comp],
id └────────────────────┘ └────────────────┘
src └──┘└────────────────────┘└┘└────────────────┘┴
typ └──┘└────────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────────────┘└──────────────────┘└──
179 simp only [linear_map.comp_apply],
id └───────────────────┘
src └─────────┘└───────────────────┘┴
typ └─────────┘└───────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────────┘└─
180 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
181 { intros h l hl₁ hl₂,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └──────────┘
st ───┘└────────────────┘└─
182 have h_bij : bij_on subtype.val (subtype.val ⁻¹' l.support.to_set : set s) l.support.to_set,
id └────┘ └─────────┘ └─┘ └─┘ ┴ └──────────────┘
src └───────────┘└────┘┴ ┴ └─────────┘┴└─┘┴ └─┘└─┘┴ └┘└──────────────┘
typ └───────────┘└────┘┴ ┴ └─────────┘┴└─┘┴ └─┘└─┘┴┴└┘└──────────────┘
doc └───────────┘└────┘┴ ┴ ┴└─┘┴ └─┘ ┴ └┘└──────────────┘
txt └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └───────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid └────────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
183 { apply bij_on.mk,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└─────────────┘└─
184 { unfold maps_to },
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘┴
st ───────┘└─────────────┘└┘└
185 { apply set.inj_on_of_injective _ subtype.val_injective },
id └─────────────────────┘ └───────────────────┘
src └────┘└─────────────────────┘└─┘└───────────────────┘┴
typ └────┘└─────────────────────┘└─┘└───────────────────┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────┘└────────────────────────────────────────────────────┘└┘└
186 intros i hi,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────────┘└─
187 rw mem_image,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
188 use subtype.mk i (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ s) hi),
id └────────┘ ┴ └───────────────────┘ └─┘ ┴ └───────┘ ┴ ┴ └┘
src └──┘└────────┘┴ ┴ └───────────────────┘└──────┘ └─┘┴ └───────┘└┘┴┴ └┘ ┴
typ └──┘└────────┘┴┴┴ └───────────────────┘└──────┘└─┘└─┘┴ └───────┘└┘┴┴┴└┘└┘┴
doc └──┘ ┴ ┴ └──────┘ └─┘ └┘ ┴ └┘ ┴
txt └──┘ ┴ ┴ └──────┘ └─┘ └┘ ┴ └┘ ┴
par └──┘ ┴ ┴ └──────┘ └─┘ └┘ ┴ └┘ ┴
pid ┴ ┴ ┴ └──────┘ └─┘ └┘ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
189 rw mem_preimage,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
190 exact ⟨hi, rfl⟩ },
id └┘ └─┘
src └────┘ └┘└─┘└┘
typ └────┘ └┘└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ─────────────────────┘└┘└
191 show l = 0,
id ┴ ┴
src └───┘ ┴┴└┘
typ └───┘┴┴┴└┘
doc └───┘ ┴ └┘
txt └───┘ ┴ └┘
par └───┘ ┴ └┘
pid └───┘ ┴ ┴┴
st ────────────────
192 { apply finsupp.eq_zero_of_comap_domain_eq_zero (subtype.val : s → ι) _ h_bij,
id └─────────────────────────────────────┘ └─────────┘ ┴ ┴ └───┘
src └────┘└─────────────────────────────────────┘┴ └─────────┘└─┘ ┴ ┴ └──┘
typ └────┘└─────────────────────────────────────┘┴ └─────────┘└─┘┴┴ ┴┴└──┘└───┘
doc └────┘ ┴ └─┘ ┴ ┴ └──┘
txt └────┘ ┴ └─┘ ┴ ┴ └──┘
par └────┘ ┴ └─┘ ┴ ┴ └──┘
pid ┴ ┴ └─┘ ┴ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
193 apply h,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────┘└─
194 convert hl₂,
id └─┘
src └──────┘
typ └──────┘└─┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────────┘└─
195 rw [finsupp.lmap_domain_apply, finsupp.map_domain_comap_domain],
id └───────────────────────┘ └─────────────────────────────┘
src └──┘└───────────────────────┘└┘└─────────────────────────────┘┴
typ └──┘└───────────────────────┘└┘└─────────────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────────────┘└───────────────────────────────┘└──
196 apply subtype.val_injective,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└─
197 rw subtype.range_val,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────┘└─
198 exact (finsupp.mem_supported _ _).1 hl₁ } },
id └───────────────────┘ └─┘
src └────┘ └───────────────────┘└──────┘ ┴
typ └────┘ └───────────────────┘└──────┘└─┘┴
doc └────┘ └──────┘ ┴
txt └────┘ └──────┘ ┴
par └────┘ └──────┘ ┴
pid ┴ └──────┘ ┴
st ─────────────────────────────────────────────┘└──┘└
199 { intros h l hl,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ────────────────┘└─
200 have hl' : finsupp.total ι M R v (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) = 0,
id └───────────┘ ┴ ┴ ┴ ┴ └────────────────┘ └─────────┘ └───────────────────┘ ┴
src └─────────┘└───────────┘┴ ┴ ┴ ┴ ┴ └────────────────┘┴ └─────────┘└┘└───────────────────┘└┘ └┘ └┘
typ └─────────┘└───────────┘┴┴┴┴┴┴┴┴┴ └────────────────┘┴ └─────────┘└┘└───────────────────┘└┘┴└┘ └┘
doc └─────────┘└───────────┘┴ ┴ ┴ ┴ ┴ └────────────────┘┴ └┘ └┘ └┘ └┘
txt └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘
par └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
201 { rw finsupp.emb_domain_eq_map_domain ⟨subtype.val, subtype.val_injective⟩ l,
id └──────────────────────────────┘ └─────────┘ └───────────────────┘ ┴
src └─┘└──────────────────────────────┘┴ └─────────┘└┘└───────────────────┘└┘
typ └─┘└──────────────────────────────┘┴ └─────────┘└┘└───────────────────┘└┘┴
doc └─┘ ┴ └┘ └┘
txt └─┘ ┴ └┘ └┘
par └─┘ ┴ └┘ └┘
pid ┴ ┴ └┘ └┘
st ─────┘└────────────────────────────────────────────────────────────────────────┘└─
202 apply hl },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────┘└┘└
203 apply finsupp.emb_domain_inj.1,
id └────────────────────┘
src └────┘└────────────────────┘└┘
typ └────┘└────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────────────┘└─
204 rw [h (finsupp.emb_domain ⟨subtype.val, subtype.val_injective⟩ l) _ hl',
id ┴ └────────────────┘ └─────────┘ └───────────────────┘ ┴ └─┘
src └──┘ ┴ └────────────────┘┴ └─────────┘└┘└───────────────────┘└┘ └──┘ └─
typ └──┘┴┴ └────────────────┘┴ └─────────┘└┘└───────────────────┘└┘┴└──┘└─┘└─
doc └──┘ ┴ └────────────────┘┴ └┘ └┘ └──┘ └─
txt └──┘ ┴ ┴ └┘ └┘ └──┘ └─
par └──┘ ┴ ┴ └┘ └┘ └──┘ └─
pid └┘ ┴ ┴ └┘ └┘ └──┘ └─
st ──────────────────────────────────────────────────────────────────────────┘└─
205 finsupp.emb_domain_zero],
id └─────────────────────┘
src ───────┘└─────────────────────┘┴
typ ───────┘└─────────────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ──────────────────────────────┘└──
206 rw [finsupp.mem_supported, finsupp.support_emb_domain],
id └───────────────────┘ └────────────────────────┘
src └──┘└───────────────────┘└┘└────────────────────────┘┴
typ └──┘└───────────────────┘└┘└────────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────────┘└──────────────────────────┘└──
207 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
208 rw [finset.mem_coe, finset.mem_map] at hx,
id └────────────┘ └────────────┘
src └──┘└────────────┘└┘└────────────┘└─────┘
typ └──┘└────────────┘└┘└────────────┘└─────┘
doc └──┘ └┘ └─────┘
txt └──┘ └┘ └─────┘
par └──┘ └┘ └─────┘
pid └┘ └┘ ┴└────┘
st ─────────────────────┘└──────────────┘┴└────┘└─
209 rcases hx with ⟨i, x', hx'⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ──────────────────────────────┘└─
210 rw ←hx',
id └─┘
src └──┘
typ └──┘└─┘
doc └──┘
txt └──┘
par └──┘
pid └┘
st ──────────┘└─
211 simp }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
212 end
st ──┘
213
214 theorem linear_independent_subtype {s : set M} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
215 linear_independent R (λ x, x : s → M) ↔
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
216 ∀ l ∈ (finsupp.supported R R s), (finsupp.total M M R id) l = 0 → l = 0 :=
id ┴ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └───────────────┘ └───────────┘ └┘ ┴ ┴
typ ┴ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └───────────┘
217 by apply @linear_independent_comp_subtype _ _ _ id
id └─────────────────────────────┘ └┘
src └────┘ └─────────────────────────────┘└─────┘└┘└
typ └────┘ └─────────────────────────────┘└─────┘└┘└
doc └────┘ └─────┘ └
txt └────┘ └─────┘ └
par └────┘ └─────┘ └
pid ┴ └─────┘ └
st └────────────────────────────────────────────────
218
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
219 theorem linear_independent_comp_subtype_disjoint {s : set ι} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
220 linear_independent R (v ∘ subtype.val : s → M) ↔
id └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └────────────────┘ ┴ └─────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
doc └────────────────┘
221 disjoint (finsupp.supported R R s) (finsupp.total ι M R v).ker :=
id └──────┘ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─┘
src └──────┘ └───────────────┘ └───────────┘ └─┘
typ └──────┘ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─┘
doc └──────┘ └───────────┘ └─┘
222 by rw [linear_independent_comp_subtype, linear_map.disjoint_ker]
id └─────────────────────────────┘ └─────────────────────┘
src └──┘└─────────────────────────────┘└┘└─────────────────────┘└─
typ └──┘└─────────────────────────────┘└┘└─────────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────────────────┘└───────────────────────┘┴└
223
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
224 theorem linear_independent_subtype_disjoint {s : set M} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
225 linear_independent R (λ x, x : s → M) ↔
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
226 disjoint (finsupp.supported R R s) (finsupp.total M M R id).ker :=
id └──────┘ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ └─┘
src └──────┘ └───────────────┘ └───────────┘ └┘ └─┘
typ └──────┘ └───────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └┘ └─┘
doc └──────┘ └───────────┘ └─┘
227 by apply @linear_independent_comp_subtype_disjoint _ _ _ id
id └──────────────────────────────────────┘ └┘
src └────┘ └──────────────────────────────────────┘└─────┘└┘└
typ └────┘ └──────────────────────────────────────┘└─────┘└┘└
doc └────┘ └─────┘ └
txt └────┘ └─────┘ └
par └────┘ └─────┘ └
pid ┴ └─────┘ └
st └─────────────────────────────────────────────────────────
228
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
229 theorem linear_independent_iff_total_on {s : set M} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
230 linear_independent R (λ x, x : s → M) ↔ (finsupp.total_on M M R id s).ker = ⊥ :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴
src └────────────────┘ ┴ └──────────────┘ └┘ └─┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴
doc └────────────────┘ └─┘
231 by rw [finsupp.total_on, linear_map.ker, linear_map.comap_cod_restrict, map_bot, comap_bot,
id └──────────────┘ └────────────┘ └───────────────────────────┘ └─────┘ └───────┘
src └──┘└──────────────┘└┘└────────────┘└┘└───────────────────────────┘└┘└─────┘└┘└───────┘└─
typ └──┘└──────────────┘└┘└────────────┘└┘└───────────────────────────┘└┘└─────┘└┘└───────┘└─
doc └──┘ └┘└────────────┘└┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └─
st └───────────────────┘└──────────────┘└─────────────────────────────┘└───────┘└─────────┘└─
232 linear_map.ker_comp, linear_independent_subtype_disjoint, disjoint, ← map_comap_subtype,
id └─────────────────┘ └─────────────────────────────────┘ └──────┘ └───────────────┘
src ─┘└─────────────────┘└┘└─────────────────────────────────┘└┘└──────┘└──┘└───────────────┘└─
typ ─┘└─────────────────┘└┘└─────────────────────────────────┘└┘└──────┘└──┘└───────────────┘└─
doc ─┘ └┘ └┘└──────┘└──┘ └─
txt ─┘ └┘ └┘ └──┘ └─
par ─┘ └┘ └┘ └──┘ └─
pid ─┘ └┘ └┘ └──┘ └─
st ────────────────────┘└───────────────────────────────────┘└────────┘└───────────────────┘└─
233 map_le_iff_le_comap, comap_bot, ker_subtype, le_bot_iff]
id └─────────────────┘ └───────┘ └─────────┘ └────────┘
src ─┘└─────────────────┘└┘└───────┘└┘└─────────┘└┘└────────┘└─
typ ─┘└─────────────────┘└┘└───────┘└┘└─────────┘└┘└────────┘└─
doc ─┘ └┘ └┘ └┘ └─
txt ─┘ └┘ └┘ └┘ └─
par ─┘ └┘ └┘ └┘ └─
pid ─┘ └┘ └┘ └┘ ┴└
st ────────────────────┘└─────────┘└───────────┘└──────────┘┴└
234
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
235 lemma linear_independent.to_subtype_range
236 (hv : linear_independent R v) : linear_independent R (λ x, x : range v → M) :=
id └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └────────────────┘ └────────────────┘ └───┘
typ └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └────────────────┘ └────────────────┘ └───┘
237 begin
st └─────
238 by_cases zero_eq_one : (0 : R) = 1,
id ┴ ┴
src └───────┘ └─┘ └──┘ └┘┴└┘
typ └───────┘ └─┘ └──┘┴└┘┴└┘
doc └───────┘ └─┘ └──┘ └┘ └┘
txt └───────┘ └─┘ └──┘ └┘ └┘
par └───────┘ └─┘ └──┘ └┘ └┘
pid ┴ └─┘ └──┘ └┘ ┴┴
st ───────────────────────────────────┘└─
239 { apply linear_independent_of_zero_eq_one zero_eq_one },
id └───────────────────────────────┘ └─────────┘
src └────┘└───────────────────────────────┘┴ ┴
typ └────┘└───────────────────────────────┘┴└─────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───┘└──────────────────────────────────────────────────┘└┘└
240 rw linear_independent_subtype,
id └────────────────────────┘
src └─┘└────────────────────────┘
typ └─┘└────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────────┘└─
241 intros l hl₁ hl₂,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
242 have h_bij : bij_on v (v ⁻¹' finset.to_set (l.support)) (finset.to_set (l.support)),
id └────┘ ┴ └─┘ └───────────┘ └───────┘
src └───────────┘└────┘┴ ┴ ┴└─┘┴ ┴ └─┘ └───────────┘┴ └───────┘└┘
typ └───────────┘└────┘┴ ┴ ┴┴└─┘┴ ┴ └─┘ └───────────┘┴ └───────┘└┘
doc └───────────┘└────┘┴ ┴ ┴└─┘┴ ┴ └─┘ └───────────┘┴ └┘
txt └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
243 { apply bij_on.mk,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────┘└─
244 { unfold maps_to },
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘┴
st ─────┘└─────────────┘└┘└
245 { apply set.inj_on_of_injective _ (linear_independent.injective zero_eq_one hv) },
id └─────────────────────┘ └──────────────────────────┘ └─────────┘ └┘
src └────┘└─────────────────────┘└─┘ └──────────────────────────┘┴ ┴ └┘
typ └────┘└─────────────────────┘└─┘ └──────────────────────────┘┴└─────────┘┴└┘└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────┘└────────────────────────────────────────────────────────────────────────────┘└┘└
246 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
247 rcases mem_range.1 (((finsupp.mem_supported _ _).1 hl₁ : ↑(l.support) ⊆ range v) hx) with ⟨i, hi⟩,
id └───────┘ └───────────────────┘ └─┘ ┴ └───────┘ ┴ └───┘ ┴ └┘
src └─────┘└───────┘└─┘ └───────────────────┘└──────┘ └─┘┴ └───────┘└┘┴┴└───┘┴ └┘ └────────────┘
typ └─────┘└───────┘└─┘ └───────────────────┘└──────┘└─┘└─┘┴ └───────┘└┘┴┴└───┘┴┴└┘└┘└────────────┘
doc └─────┘ └─┘ └──────┘ └─┘ └┘ ┴└───┘┴ └┘ └────────────┘
txt └─────┘ └─┘ └──────┘ └─┘ └┘ ┴ ┴ └┘ └────────────┘
par └─────┘ └─┘ └──────┘ └─┘ └┘ ┴ ┴ └┘ └────────────┘
pid ┴ └─┘ └──────┘ └─┘ └┘ ┴ ┴ └┘ └────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248 rw mem_image,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
249 use i,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ────────┘└─
250 rw [mem_preimage, hi],
id └──────────┘ └┘
src └──┘└──────────┘└┘ ┴
typ └──┘└──────────┘└┘└┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────┘└──┘└──
251 exact ⟨hx, rfl⟩ },
id └┘ └─┘
src └────┘ └┘└─┘└┘
typ └────┘ └┘└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ───────────────────┘└┘└
252 apply finsupp.eq_zero_of_comap_domain_eq_zero v l,
id └─────────────────────────────────────┘ ┴ ┴
src └────┘└─────────────────────────────────────┘┴ ┴
typ └────┘└─────────────────────────────────────┘┴┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────────────┘└─
253 apply linear_independent_iff.1 hv,
id └────────────────────┘ └┘
src └────┘└────────────────────┘└─┘
typ └────┘└────────────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────────────────────────┘└─
254 rw [finsupp.total_comap_domain, finset.sum_preimage v l.support h_bij (λ (x : M), l x • x)],
id └────────────────────────┘ └─────────────────┘ ┴ └───────┘ └───┘ ┴ ┴ ┴
src └──┘└────────────────────────┘└┘└─────────────────┘┴ ┴└───────┘┴ ┴ └────┘ └─┘ ┴ ┴┴┴ └┘
typ └──┘└────────────────────────┘└┘└─────────────────┘┴┴┴└───────┘┴└───┘┴ └────┘┴└─┘┴┴ ┴┴┴ └┘
doc └──┘ └┘ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘
txt └──┘ └┘ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘
par └──┘ └┘ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘
pid └┘ └┘ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘
st ───────────────────────────────┘└──────────────────────────────────────────────────────────┘└──
255 rw [finsupp.total_apply, finsupp.sum] at hl₂,
id └─────────────────┘ └─────────┘
src └──┘└─────────────────┘└┘└─────────┘└──────┘
typ └──┘└─────────────────┘└┘└─────────┘└──────┘
doc └──┘ └┘└─────────┘└──────┘
txt └──┘ └┘ └──────┘
par └──┘ └┘ └──────┘
pid └┘ └┘ ┴└─────┘
st ────────────────────────┘└───────────┘┴└─────┘└─
256 apply hl₂
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────┘
257 end
st └─┘
258
259 lemma linear_independent.of_subtype_range (hv : injective v)
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
260 (h : linear_independent R (λ x, x : range v → M)) : linear_independent R v :=
id └────────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────────┘ └───┘ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘ └───┘ └────────────────┘
261 begin
st └─────
262 rw linear_independent_iff,
id └────────────────────┘
src └─┘└────────────────────┘
typ └─┘└────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────┘└─
263 intros l hl,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
264 apply finsupp.injective_map_domain hv,
id └──────────────────────────┘ └┘
src └────┘└──────────────────────────┘┴
typ └────┘└──────────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────┘└─
265 apply linear_independent_subtype.1 h (l.map_domain v),
id └────────────────────────┘ ┴ └──────────┘ ┴
src └────┘└────────────────────────┘└─┘ ┴ └──────────┘┴ ┴
typ └────┘└────────────────────────┘└─┘┴┴ └──────────┘┴┴┴
doc └────┘ └─┘ ┴ └──────────┘┴ ┴
txt └────┘ └─┘ ┴ ┴ ┴
par └────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
266 { rw finsupp.mem_supported,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└──────────────────────┘└─
267 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
268 have := finset.mem_coe.2 (finsupp.map_domain_support hx),
id └────────────┘ └────────────────────────┘ └┘
src └──────┘└────────────┘└─┘ └────────────────────────┘┴ ┴
typ └──────┘└────────────┘└─┘ └────────────────────────┘┴└┘┴
doc └──────┘ └─┘ ┴ ┴
txt └──────┘ └─┘ ┴ ┴
par └──────┘ └─┘ ┴ ┴
pid └───┘└─┘ └─┘ ┴ ┴
st ───────────────────────────────────────────────────────────┘└─
269 rw finset.coe_image at this,
id └──────────────┘
src └─┘└──────────────┘└──────┘
typ └─┘└──────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────────────────┘└─
270 apply set.image_subset_range _ _ this, },
id └────────────────────┘ └──┘
src └────┘└────────────────────┘└───┘
typ └────┘└────────────────────┘└───┘└──┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └───┘
st ────────────────────────────────────────┘└──┘└
271 { rwa [finsupp.total_map_domain _ _ hv, left_id] }
id └──────────────────────┘ └┘ └─────┘
src └───┘└──────────────────────┘└───┘ └┘└─────┘└┘
typ └───┘└──────────────────────┘└───┘└┘└┘└─────┘└┘
doc └───┘ └───┘ └┘ └┘
txt └───┘ └───┘ └┘ └┘
par └───┘ └───┘ └┘ └┘
pid └┘ └───┘ └┘ ┴┴
st ───────────────────────────────────────┘└───────┘┴┴└─
272 end
st ──┘
273
274 lemma linear_independent.restrict_of_comp_subtype {s : set ι}
id └─┘ ┴
src └─┘
typ └─┘ ┴
275 (hs : linear_independent R (v ∘ subtype.val : s → M)) :
id └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └────────────────┘ ┴ └─────────┘
typ └────────────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └────────────────┘
276 linear_independent R (function.restrict v s) :=
id └────────────────┘ ┴ └───────────────┘ ┴ ┴
src └────────────────┘ └───────────────┘
typ └────────────────┘ ┴ └───────────────┘ ┴ ┴
doc └────────────────┘
277 begin
st └─────
278 have h_restrict : restrict v s = v ∘ (λ x, x.val) := rfl,
id └──────┘ ┴ ┴ ┴ ┴ └──┘ └─┘
src └────────────────┘└──────┘┴ ┴ ┴┴┴ ┴┴┴ └──┘ └──┘└───┘└─┘
typ └────────────────┘└──────┘┴ ┴┴┴┴┴┴┴┴┴ └──┘ └──┘└───┘└─┘
doc └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘
txt └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘
par └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───┘
pid └─────────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└──┘
st ─────────────────────────────────────────────────────────┘└─
279 rw [linear_independent_iff, h_restrict, finsupp.total_comp],
id └────────────────────┘ └────────┘ └────────────────┘
src └──┘└────────────────────┘└┘ └┘└────────────────┘┴
typ └──┘└────────────────────┘└┘└────────┘└┘└────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────────────────────────┘└──────────┘└──────────────────┘└──
280 intros l hl,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
281 have h_map_domain_subtype_eq_0 : l.map_domain subtype.val = 0,
id └──────────┘ └─────────┘
src └───────────────────────────────┘└──────────┘┴└─────────┘┴ └┘
typ └───────────────────────────────┘└──────────┘┴└─────────┘┴ └┘
doc └───────────────────────────────┘└──────────┘┴ ┴ └┘
txt └───────────────────────────────┘ ┴ ┴ └┘
par └───────────────────────────────┘ ┴ ┴ └┘
pid └────────────────────────────┘└─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────┘└─
282 { rw linear_independent_comp_subtype at hs,
id └─────────────────────────────┘
src └─┘└─────────────────────────────┘└────┘
typ └─┘└─────────────────────────────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ───┘└──────────────────────────────────────┘└─
283 apply hs (finsupp.lmap_domain R R (λ x : subtype s, x.val) l) _ hl,
id └┘ └─────────────────┘ ┴ └─────┘ ┴ ┴ └┘
src └────┘ ┴ └─────────────────┘┴ ┴ ┴ └───┘└─────┘┴ └┘ └┘ └──┘
typ └────┘└┘┴ └─────────────────┘┴ ┴┴┴ └───┘└─────┘┴┴└┘ └┘┴└──┘└┘
doc └────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └┘ └──┘
txt └────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └┘ └──┘
par └────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └┘ └──┘
pid ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └┘ └┘ └──┘
st ─────────────────────────────────────────────────────────────────────┘└─
284 rw finsupp.mem_supported,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────┘└─
285 simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
286 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
287 have := finset.mem_coe.2 (finsupp.map_domain_support (finset.mem_coe.1 hx)),
id └────────────────────────┘ └────────────┘ └┘
src └──────┘ └─┘ └────────────────────────┘┴ └────────────┘└─┘ └┘
typ └──────┘ └─┘ └────────────────────────┘┴ └────────────┘└─┘└┘└┘
doc └──────┘ └─┘ ┴ └─┘ └┘
txt └──────┘ └─┘ ┴ └─┘ └┘
par └──────┘ └─┘ ┴ └─┘ └┘
pid └───┘└─┘ └─┘ ┴ └─┘ └┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
288 rw finset.coe_image at this,
id └──────────────┘
src └─┘└──────────────┘└──────┘
typ └─┘└──────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────────────────┘└─
289 exact subtype.val_image_subset _ _ this },
id └──────────────────────┘ └──┘
src └────┘└──────────────────────┘└───┘ ┴
typ └────┘└──────────────────────┘└───┘└──┘┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ───────────────────────────────────────────┘└┘└
290 apply @finsupp.injective_map_domain _ (subtype s) ι,
id └──────────────────────────┘ └─────┘ ┴ ┴
src └────┘ └──────────────────────────┘└─┘ └─────┘┴ └┘
typ └────┘ └──────────────────────────┘└─┘ └─────┘┴┴└┘┴
doc └────┘ └─┘ ┴ └┘
txt └────┘ └─┘ ┴ └┘
par └────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ └┘
st ────────────────────────────────────────────────────┘└─
291 { apply subtype.val_injective },
id └───────────────────┘
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────────────────────────┘└┘└
292 { simpa },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└──
293 end
st ──┘
294
295 lemma linear_independent_empty : linear_independent R (λ x, x : (∅ : set M) → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴
src └────────────────┘ ┴ └─┘
typ └────────────────┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴
doc └────────────────┘
296 by simp [linear_independent_subtype_disjoint]
id └─────────────────────────────────┘
src └────┘└─────────────────────────────────┘└─
typ └────┘└─────────────────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────────────────────────
297
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
298 lemma linear_independent.mono {t s : set M} (h : t ⊆ s) :
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
299 linear_independent R (λ x, x : s → M) → linear_independent R (λ x, x : t → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────┘
300 begin
st └─────
301 simp only [linear_independent_subtype_disjoint],
id └─────────────────────────────────┘
src └─────────┘└─────────────────────────────────┘┴
typ └─────────┘└─────────────────────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───────────────────────────────────────────────┘└─
302 exact (disjoint_mono_left (finsupp.supported_mono h))
id └────────────────┘ └────────────────────┘ ┴
src └────┘ └────────────────┘┴ └────────────────────┘┴ └─┘
typ └────┘ └────────────────┘┴ └────────────────────┘┴┴└─┘
doc └────┘ ┴ ┴ └─┘
txt └────┘ ┴ ┴ └─┘
par └────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └┘┴
st ──────────────────────────────────────────────────────┘
303 end
st └─┘
304
305 lemma linear_independent_union {s t : set M}
id └─┘ ┴
src └─┘
typ └─┘ ┴
306 (hs : linear_independent R (λ x, x : s → M)) (ht : linear_independent R (λ x, x : t → M))
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────┘
307 (hst : disjoint (span R s) (span R t)) :
id └──────┘ └──┘ ┴ ┴ └──┘ ┴ ┴
src └──────┘ └──┘ └──┘
typ └──────┘ └──┘ ┴ ┴ └──┘ ┴ ┴
doc └──────┘ └──┘ └──┘
308 linear_independent R (λ x, x : (s ∪ t) → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
309 begin
st └─────
310 rw [linear_independent_subtype_disjoint, disjoint_def, finsupp.supported_union],
id └─────────────────────────────────┘ └──────────┘ └─────────────────────┘
src └──┘└─────────────────────────────────┘└┘└──────────┘└┘└─────────────────────┘┴
typ └──┘└─────────────────────────────────┘└┘└──────────┘└┘└─────────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ────────────────────────────────────────┘└────────────┘└───────────────────────┘└──
311 intros l h₁ h₂, rw mem_sup at h₁,
id └─────┘
src └────────────┘ └─┘└─────┘└────┘
typ └────────────┘ └─┘└─────┘└────┘
doc └────────────┘ └─┘ └────┘
txt └────────────┘ └─┘ └────┘
par └────────────┘ └─┘ └────┘
pid └──────┘ ┴ └────┘
st ───────────────┘└────────────────┘└─
312 rcases h₁ with ⟨ls, hls, lt, hlt, rfl⟩,
id └┘
src └─────┘ └───────────────────────────┘
typ └─────┘└┘└───────────────────────────┘
doc └─────┘ └───────────────────────────┘
txt └─────┘ └───────────────────────────┘
par └─────┘ └───────────────────────────┘
pid ┴ └───────────────────────────┘
st ───────────────────────────────────────┘└─
313 have h_ls_mem_t : finsupp.total M M R id ls ∈ span R t,
id └───────────┘ ┴ └┘ └┘ ┴ └──┘ ┴ ┴
src └────────────────┘└───────────┘┴ ┴ ┴ ┴└┘┴ ┴┴┴└──┘┴ ┴
typ └────────────────┘└───────────┘┴ ┴┴┴ ┴└┘┴└┘┴┴┴└──┘┴┴┴┴
doc └────────────────┘└───────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴
txt └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
314 { rw [← image_id t, finsupp.span_eq_map_total],
id └──────┘ ┴ └───────────────────────┘
src └────┘└──────┘┴ └┘└───────────────────────┘┴
typ └────┘└──────┘┴┴└┘└───────────────────────┘┴
doc └────┘ ┴ └┘ ┴
txt └────┘ ┴ └┘ ┴
par └────┘ ┴ └┘ ┴
pid └──┘ ┴ └┘ ┴
st ───┘└──────────────┘└─────────────────────────┘└──
315 apply (add_mem_iff_left (map _ _) (mem_image_of_mem _ hlt)).1,
id └──────────────┘ └─┘ └──────────────┘ └─┘
src └────┘ └──────────────┘┴ └─┘└────┘ └──────────────┘└─┘ └──┘
typ └────┘ └──────────────┘┴ └─┘└────┘ └──────────────┘└─┘└─┘└──┘
doc └────┘ ┴ └─┘└────┘ └─┘ └──┘
txt └────┘ ┴ └────┘ └─┘ └──┘
par └────┘ ┴ └────┘ └─┘ └──┘
pid ┴ ┴ └────┘ └─┘ └┘└┘
st ────────────────────────────────────────────────────────────────┘└─
316 rw [← linear_map.map_add, linear_map.mem_ker.1 h₂],
id └────────────────┘ └────────────────┘ └┘
src └────┘└────────────────┘└┘└────────────────┘└─┘ ┴
typ └────┘└────────────────┘└┘└────────────────┘└─┘└┘┴
doc └────┘ └┘ └─┘ ┴
txt └────┘ └┘ └─┘ ┴
par └────┘ └┘ └─┘ ┴
pid └──┘ └┘ └─┘ ┴
st ───────────────────────────┘└───────────────────────┘└──
317 apply zero_mem },
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└┘└
318 have h_lt_mem_s : finsupp.total M M R id lt ∈ span R s,
id └───────────┘ ┴ └┘ └┘ └──┘ ┴ ┴
src └────────────────┘└───────────┘┴ ┴ ┴ ┴└┘┴ ┴ ┴└──┘┴ ┴
typ └────────────────┘└───────────┘┴ ┴┴┴ ┴└┘┴└┘┴ ┴└──┘┴┴┴┴
doc └────────────────┘└───────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴
txt └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
319 { rw [← image_id s, finsupp.span_eq_map_total],
id └──────┘ ┴ └───────────────────────┘
src └────┘└──────┘┴ └┘└───────────────────────┘┴
typ └────┘└──────┘┴┴└┘└───────────────────────┘┴
doc └────┘ ┴ └┘ ┴
txt └────┘ ┴ └┘ ┴
par └────┘ ┴ └┘ ┴
pid └──┘ ┴ └┘ ┴
st ───┘└──────────────┘└─────────────────────────┘└──
320 apply (add_mem_iff_left (map _ _) (mem_image_of_mem _ hls)).1,
id └──────────────┘ └─┘ └──────────────┘ └─┘
src └────┘ └──────────────┘┴ └─┘└────┘ └──────────────┘└─┘ └──┘
typ └────┘ └──────────────┘┴ └─┘└────┘ └──────────────┘└─┘└─┘└──┘
doc └────┘ ┴ └─┘└────┘ └─┘ └──┘
txt └────┘ ┴ └────┘ └─┘ └──┘
par └────┘ ┴ └────┘ └─┘ └──┘
pid ┴ ┴ └────┘ └─┘ └┘└┘
st ────────────────────────────────────────────────────────────────┘└─
321 rw [← linear_map.map_add, add_comm, linear_map.mem_ker.1 h₂],
id └────────────────┘ └──────┘ └────────────────┘ └┘
src └────┘└────────────────┘└┘└──────┘└┘└────────────────┘└─┘ ┴
typ └────┘└────────────────┘└┘└──────┘└┘└────────────────┘└─┘└┘┴
doc └────┘ └┘ └┘ └─┘ ┴
txt └────┘ └┘ └┘ └─┘ ┴
par └────┘ └┘ └┘ └─┘ ┴
pid └──┘ └┘ └┘ └─┘ ┴
st ───────────────────────────┘└────────┘└───────────────────────┘└──
322 apply zero_mem },
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘└┘└
323 have h_ls_mem_s : (finsupp.total M M R id) ls ∈ span R s,
id └───────────┘ ┴ └┘ └┘ └──┘ ┴ ┴
src └────────────────┘ └───────────┘┴ ┴ ┴ ┴└┘└┘ ┴ ┴└──┘┴ ┴
typ └────────────────┘ └───────────┘┴ ┴┴┴ ┴└┘└┘└┘┴ ┴└──┘┴┴┴┴
doc └────────────────┘ └───────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘┴ ┴
txt └────────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └────────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
324 { rw ← image_id s,
id └──────┘ ┴
src └───┘└──────┘┴
typ └───┘└──────┘┴┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ───┘└─────────────┘└─
325 apply (finsupp.mem_span_iff_total _).2 ⟨ls, hls, rfl⟩ },
id └────────────────────────┘ └┘ └─┘ └─┘
src └────┘ └────────────────────────┘└────┘ └┘ └┘└─┘└┘
typ └────┘ └────────────────────────┘└────┘ └┘└┘└─┘└┘└─┘└┘
doc └────┘ └────┘ └┘ └┘ └┘
txt └────┘ └────┘ └┘ └┘ └┘
par └────┘ └────┘ └┘ └┘ └┘
pid ┴ └────┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────┘└┘└
326 have h_lt_mem_t : (finsupp.total M M R id) lt ∈ span R t,
id └───────────┘ ┴ └┘ └┘ └──┘ ┴ ┴
src └────────────────┘ └───────────┘┴ ┴ ┴ ┴└┘└┘ ┴ ┴└──┘┴ ┴
typ └────────────────┘ └───────────┘┴ ┴┴┴ ┴└┘└┘└┘┴ ┴└──┘┴┴┴┴
doc └────────────────┘ └───────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘┴ ┴
txt └────────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └────────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └─────────────┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
327 { rw ← image_id t,
id └──────┘ ┴
src └───┘└──────┘┴
typ └───┘└──────┘┴┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ───┘└─────────────┘└─
328 apply (finsupp.mem_span_iff_total _).2 ⟨lt, hlt, rfl⟩ },
id └────────────────────────┘ └┘ └─┘ └─┘
src └────┘ └────────────────────────┘└────┘ └┘ └┘└─┘└┘
typ └────┘ └────────────────────────┘└────┘ └┘└┘└─┘└┘└─┘└┘
doc └────┘ └────┘ └┘ └┘ └┘
txt └────┘ └────┘ └┘ └┘ └┘
par └────┘ └────┘ └┘ └┘ └┘
pid ┴ └────┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────┘└┘└
329 have h_ls_0 : ls = 0 :=
id └┘ ┴
src └────────────┘ ┴┴└─────
typ └────────────┘└┘┴┴└─────
doc └────────────┘ ┴ └─────
txt └────────────┘ ┴ └─────
par └────────────┘ ┴ └─────
pid └─────────┘└─┘ ┴ ┴└────
st ──────────────────────────
330 disjoint_def.1 (linear_independent_subtype_disjoint.1 hs) _ hls
id └─────────────────────────────────┘ └┘ └─┘
src ───┘ └─┘ └─────────────────────────────────┘└─┘ └──┘ └
typ ───┘ └─┘ └─────────────────────────────────┘└─┘└┘└──┘└─┘└
doc ───┘ └─┘ └─┘ └──┘ └
txt ───┘ └─┘ └─┘ └──┘ └
par ───┘ └─┘ └─┘ └──┘ └
pid ───┘ └─┘ └─┘ └──┘ └
st ────────────────────────────────────────────────────────────────────
331 (linear_map.mem_ker.2 $ disjoint_def.1 hst (finsupp.total M M R id ls) h_ls_mem_s h_ls_mem_t),
id └────────────────┘ └──────────┘ └─┘ └───────────┘ ┴ ┴ └┘ └┘ └────────┘ └────────┘
src ───┘ └────────────────┘└─┘ ┴└──────────┘└─┘ ┴ └───────────┘┴ ┴ ┴ ┴└┘┴ └┘ ┴ ┴
typ ───┘ └────────────────┘└─┘ ┴└──────────┘└─┘└─┘┴ └───────────┘┴ ┴┴┴┴┴└┘┴└┘└┘└────────┘┴└────────┘┴
doc ───┘ └─┘ ┴ └─┘ ┴ └───────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
txt ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
332 have h_lt_0 : lt = 0 :=
id └┘
src └────────────┘ ┴ └─────
typ └────────────┘└┘┴ └─────
doc └────────────┘ ┴ └─────
txt └────────────┘ ┴ └─────
par └────────────┘ ┴ └─────
pid └─────────┘└─┘ ┴ ┴└────
st ──────────────────────────
333 disjoint_def.1 (linear_independent_subtype_disjoint.1 ht) _ hlt
id └─────────────────────────────────┘ └┘ └─┘
src ───┘ └─┘ └─────────────────────────────────┘└─┘ └──┘ └
typ ───┘ └─┘ └─────────────────────────────────┘└─┘└┘└──┘└─┘└
doc ───┘ └─┘ └─┘ └──┘ └
txt ───┘ └─┘ └─┘ └──┘ └
par ───┘ └─┘ └─┘ └──┘ └
pid ───┘ └─┘ └─┘ └──┘ └
st ────────────────────────────────────────────────────────────────────
334 (linear_map.mem_ker.2 $ disjoint_def.1 hst (finsupp.total M M R id lt) h_lt_mem_s h_lt_mem_t),
id └────────────────┘ └──────────┘ └─┘ └───────────┘ ┴ ┴ └┘ └┘ └────────┘ └────────┘
src ───┘ └────────────────┘└─┘ ┴└──────────┘└─┘ ┴ └───────────┘┴ ┴ ┴ ┴└┘┴ └┘ ┴ ┴
typ ───┘ └────────────────┘└─┘ ┴└──────────┘└─┘└─┘┴ └───────────┘┴ ┴┴┴┴┴└┘┴└┘└┘└────────┘┴└────────┘┴
doc ───┘ └─┘ ┴ └─┘ ┴ └───────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
txt ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid ───┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
335 show ls + lt = 0,
id └┘ ┴ └┘
src └───┘ ┴┴┴ ┴ └┘
typ └───┘└┘┴┴┴└┘┴ └┘
doc └───┘ ┴ ┴ ┴ └┘
txt └───┘ ┴ ┴ ┴ └┘
par └───┘ ┴ ┴ ┴ └┘
pid └───┘ ┴ ┴ ┴ ┴┴
st ─────────────────┘
336 by simp [h_ls_0, h_lt_0],
id └────┘ └────┘
src └────┘ └┘ ┴
typ └────┘└────┘└┘└────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─
337 end
st ──┘
338
339 lemma linear_independent_of_finite (s : set M)
id └─┘ ┴
src └─┘
typ └─┘ ┴
340 (H : ∀ t ⊆ s, finite t → linear_independent R (λ x, x : t → M)) :
id ┴ ┴ └────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ └────────────────┘
typ ┴ ┴ └────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────────────────┘
341 linear_independent R (λ x, x : s → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
342 linear_independent_subtype.2 $
id └────────────────────────┘┴
src └────────────────────────┘┴
typ └────────────────────────┘┴
343 λ l hl, linear_independent_subtype.1 (H _ hl (finset.finite_to_set _)) l (subset.refl _)
id ┴ └┘ └────────────────────────┘┴ ┴ └┘ └──────────────────┘ ┴ └─────────┘
src └────────────────────────┘┴ └──────────────────┘ └─────────┘
typ ┴ └┘ └────────────────────────┘┴ ┴ └┘ └──────────────────┘ ┴ └─────────┘
344
345 lemma linear_independent_Union_of_directed {η : Type*}
346 {s : η → set M} (hs : directed (⊆) s)
id ┴ └─┘ ┴ └──────┘ ┴ ┴
src └─┘ └──────┘ ┴
typ ┴ └─┘ ┴ └──────┘ ┴ ┴
doc └──────┘
347 (h : ∀ i, linear_independent R (λ x, x : s i → M)) :
id ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
348 linear_independent R (λ x, x : (⋃ i, s i) → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────────────┘ ┴ ┴
349 begin
st └─────
350 haveI := classical.dec (nonempty η),
id └───────────┘ └──────┘ ┴
src └───────┘└───────────┘┴ └──────┘┴ ┴
typ └───────┘└───────────┘┴ └──────┘┴┴┴
doc └───────┘ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴
pid ┴└─┘ ┴ ┴ ┴
st ────────────────────────────────────┘└─
351 by_cases hη : nonempty η,
id └──────┘ ┴
src └───────┘ └─┘└──────┘┴
typ └───────┘ └─┘└──────┘┴┴
doc └───────┘ └─┘ ┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────┘└─
352 { refine linear_independent_of_finite (⋃ i, s i) (λ t ht ft, _),
id └──────────────────────────┘ ┴ ┴ ┴
src └─────┘└──────────────────────────┘┴ ┴└┘┴┴ ┴ └┘ └──────────┘
typ └─────┘└──────────────────────────┘┴ ┴└┘┴┴┴┴ └┘ └──────────┘
doc └─────┘ ┴ ┴└┘┴┴ ┴ └┘ └──────────┘
txt └─────┘ ┴ └┘ ┴ ┴ └┘ └──────────┘
par └─────┘ ┴ └┘ ┴ ┴ └┘ └──────────┘
pid ┴ ┴ └┘ ┴ ┴ └┘ └──────────┘
st ───┘└───────────────────────────────────────────────────────────┘└─
353 rcases finite_subset_Union ft ht with ⟨I, fi, hI⟩,
id └─────────────────┘ └┘ └┘
src └─────┘└─────────────────┘┴ ┴ └───────────────┘
typ └─────┘└─────────────────┘┴└┘┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ────────────────────────────────────────────────────┘└─
354 rcases hs.finset_le hη fi.to_finset with ⟨i, hi⟩,
id └──────────┘ └┘ └──────────┘
src └─────┘└──────────┘┴ ┴└──────────┘└───────────┘
typ └─────┘└──────────┘┴└┘┴└──────────┘└───────────┘
doc └─────┘ ┴ ┴└──────────┘└───────────┘
txt └─────┘ ┴ ┴ └───────────┘
par └─────┘ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ └───────────┘
st ───────────────────────────────────────────────────┘└─
355 exact (h i).mono (subset.trans hI $ bUnion_subset $
id ┴ ┴ └──────────┘ └┘ └───────────┘
src └────┘ ┴ └─────┘ └──────────┘┴ ┴ ┴└───────────┘┴ └
typ └────┘ ┴┴┴└─────┘ └──────────┘┴└┘┴ ┴└───────────┘┴ └
doc └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
txt └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
par └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
pid ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────────────────────────
356 λ j hj, hi j (finite.mem_to_finset.2 hj)) },
id └┘ └──────────────────┘
src ─────┘ └─────┘ ┴ ┴ └──────────────────┘└─┘ └─┘
typ ─────┘ └─────┘└┘┴ ┴ └──────────────────┘└─┘ └─┘
doc ─────┘ └─────┘ ┴ ┴ └─┘ └─┘
txt ─────┘ └─────┘ ┴ ┴ └─┘ └─┘
par ─────┘ └─────┘ ┴ ┴ └─┘ └─┘
pid ─────┘ └─────┘ ┴ ┴ └─┘ └┘┴
st ───────────────────────────────────────────────┘└┘└
357 { refine linear_independent_empty.mono _,
id └───────────────────────────┘
src └─────┘└───────────────────────────┘└┘
typ └─────┘└───────────────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ─────────────────────────────────────────┘└─
358 rintro _ ⟨_, ⟨i, _⟩, _⟩, exact hη ⟨i⟩ }
id └┘ ┴
src └─────────────────────┘ └────┘ ┴ └┘
typ └─────────────────────┘ └────┘└┘┴ ┴└┘
doc └─────────────────────┘ └────┘ ┴ └┘
txt └─────────────────────┘ └────┘ ┴ └┘
par └─────────────────────┘ └────┘ ┴ └┘
pid └───────────────┘ ┴ ┴ ┴┴
st ──────────────────────────┘└─────────────┘└─
359 end
st ──┘
360
361 lemma linear_independent_sUnion_of_directed {s : set (set M)}
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
362 (hs : directed_on (⊆) s)
id └─────────┘ ┴ ┴
src └─────────┘ ┴
typ └─────────┘ ┴ ┴
doc └─────────┘
363 (h : ∀ a ∈ s, linear_independent R (λ x, x : (a : set M) → M)) :
id ┴ ┴ └────────────────┘ ┴ ┴ ┴ └┘ └─┘ ┴ ┴
src └────────────────┘ └─┘
typ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴
doc └────────────────┘
364 linear_independent R (λ x, x : (⋃₀ s) → M) :=
id └────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴
src └────────────────┘ └┘
typ └────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴
doc └────────────────┘
365 by rw sUnion_eq_Union; exact
id └─────────────┘
src └─┘└─────────────┘ └────┘
typ └─┘└─────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────
366 linear_independent_Union_of_directed
id └──────────────────────────────────┘
src └──────────────────────────────────┘└
typ └──────────────────────────────────┘└
doc └
txt └
par └
pid └
st ─────────────────────────────────────
367 ((directed_on_iff_directed _).1 hs) (by simpa using h)
id └──────────────────────┘ └┘ ┴
src ─┘ └──────────────────────┘└────┘ └┘ ┴└──────────┘ └─
typ ─┘ └──────────────────────┘└────┘└┘└┘ ┴└──────────┘┴└─
doc ─┘ └────┘ └┘ ┴└──────────┘ └─
txt ─┘ └────┘ └┘ ┴└──────────┘ └─
par ─┘ └────┘ └┘ ┴└──────────┘ └─
pid ─┘ └────┘ └┘ └───────────┘ ┴└
st ────────────────────────────────────────┘└────────────┘└─
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 lemma linear_independent_bUnion_of_directed {η} {s : set η} {t : η → set M}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
370 (hs : directed_on (t ⁻¹'o (⊆)) s) (h : ∀a∈s, linear_independent R (λ x, x : t a → M)) :
id └─────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └──┘ ┴ └────────────────┘
typ └─────────┘ ┴ └──┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └──┘ └────────────────┘
371 linear_independent R (λ x, x : (⋃a∈s, t a) → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └────────────────┘ ┴ ┴
372 by rw bUnion_eq_Union; exact
id └─────────────┘
src └─┘└─────────────┘ └────┘
typ └─┘└─────────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────
373 linear_independent_Union_of_directed
id └──────────────────────────────────┘
src └──────────────────────────────────┘└
typ └──────────────────────────────────┘└
doc └
txt └
par └
pid └
st ─────────────────────────────────────
374 ((directed_comp _ _ _).2 $ (directed_on_iff_directed _).1 hs)
id └───────────┘ └──────────────────────┘ └┘
src ─┘ └───────────┘└────────┘ ┴ └──────────────────────┘└────┘ └─
typ ─┘ └───────────┘└────────┘ ┴ └──────────────────────┘└────┘└┘└─
doc ─┘ └────────┘ ┴ └────┘ └─
txt ─┘ └────────┘ ┴ └────┘ └─
par ─┘ └────────┘ ┴ └────┘ └─
pid ─┘ └────────┘ ┴ └────┘ └─
st ────────────────────────────────────────────────────────────────
375 (by simpa using h)
id ┴
src ─┘ ┴└──────────┘ └─
typ ─┘ ┴└──────────┘┴└─
doc ─┘ ┴└──────────┘ └─
txt ─┘ ┴└──────────┘ └─
par ─┘ ┴└──────────┘ └─
pid ─┘ └───────────┘ ┴└
st ────┘└────────────┘└─
376
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
377 lemma linear_independent_Union_finite_subtype {ι : Type*} {f : ι → set M}
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
378 (hl : ∀i, linear_independent R (λ x, x : f i → M))
id ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
379 (hd : ∀i, ∀t:set ι, finite t → i ∉ t → disjoint (span R (f i)) (⨆i∈t, span R (f i))) :
id ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
src └─┘ └────┘ ┴ └──────┘ └──┘ ┴ ┴ └──┘
typ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ └──────┘ └──┘ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
doc └────┘ └──────┘ └──┘ ┴ ┴ └──┘
380 linear_independent R (λ x, x : (⋃i, f i) → M) :=
id └────────────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc └────────────────┘ ┴ ┴
381 begin
st └─────
382 rw [Union_eq_Union_finset f],
id └───────────────────┘ ┴
src └──┘└───────────────────┘┴ ┴
typ └──┘└───────────────────┘┴┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ────────────────────────────┘└──
383 apply linear_independent_Union_of_directed,
id └──────────────────────────────────┘
src └────┘└──────────────────────────────────┘
typ └────┘└──────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────────────────┘└─
384 apply directed_of_sup,
id └─────────────┘
src └────┘└─────────────┘
typ └────┘└─────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
385 exact (assume t₁ t₂ ht, Union_subset_Union $ assume i, Union_subset_Union_const $ assume h, ht h),
id └────────────────┘ └──────────────────────┘
src └────┘ └─────────┘└────────────────┘┴ ┴ └──┘└──────────────────────┘┴ ┴ └──┘ ┴ ┴
typ └────┘ └─────────┘└────────────────┘┴ ┴ └──┘└──────────────────────┘┴ ┴ └──┘ ┴ ┴
doc └────┘ └─────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
txt └────┘ └─────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
par └────┘ └─────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
pid ┴ └─────────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────────┘└─
386 assume t, rw [set.Union, ← finset.sup_eq_supr],
id └───────┘ └────────────────┘
src └──────┘ └──┘└───────┘└──┘└────────────────┘┴
typ └──────┘ └──┘└───────┘└──┘└────────────────┘┴
doc └──────┘ └──┘└───────┘└──┘ ┴
txt └──────┘ └──┘ └──┘ ┴
par └──────┘ └──┘ └──┘ ┴
pid └──────┘ └┘ └──┘ ┴
st ─────────┘└─────────────┘└────────────────────┘└──
387 refine t.induction_on _ _,
id └────────────┘
src └─────┘└────────────┘└──┘
typ └─────┘└────────────┘└──┘
doc └─────┘└────────────┘└──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ──────────────────────────┘└─
388 { rw finset.sup_empty,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└─────────────────┘└─
389 apply linear_independent_empty_type (not_nonempty_iff_imp_false.2 _),
id └───────────────────────────┘ └────────────────────────┘
src └────┘└───────────────────────────┘┴ └────────────────────────┘└───┘
typ └────┘└───────────────────────────┘┴ └────────────────────────┘└───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ───────────────────────────────────────────────────────────────────────┘└─
390 exact λ x, set.not_mem_empty x (subtype.mem x) },
id └───────────────┘ └─────────┘
src └────┘ └──┘└───────────────┘┴ ┴ └─────────┘┴ └┘
typ └────┘ └──┘└───────────────┘┴ ┴ └─────────┘┴ └┘
doc └────┘ └──┘ ┴ ┴ ┴ └┘
txt └────┘ └──┘ ┴ ┴ ┴ └┘
par └────┘ └──┘ ┴ ┴ ┴ └┘
pid ┴ └──┘ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────┘└┘└
391 { rintros ⟨i⟩ s his ih,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └───────────┘
st ───────────────────────┘└─
392 rw [finset.sup_insert],
id └───────────────┘
src └──┘└───────────────┘┴
typ └──┘└───────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────────┘┴
393 apply linear_independent_union,
394 { apply hl },
st └┘
395 { apply ih },
st └┘
396 rw [finset.sup_eq_supr],
397 refine disjoint_mono (le_refl _) _ (hd i _ _ his),
id ┴ ┴
src ┴
typ ┴ ┴┴
doc ┴
txt ┴
par ┴
pid ┴
st └┘
398 { simp only [(span_Union _).symm],
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
399 refine span_mono (@supr_le_supr2 (set M) _ _ _ _ _ _),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
400 rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st └┘
401 { change finite (plift.up ⁻¹' s.to_set),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
402 exact finite_preimage (inj_on_of_injective _ (assume i j, plift.up.inj))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
403 s.finite_to_set } }
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └───
404 end
st ──┘
405
406 lemma linear_independent_Union_finite {η : Type*} {ιs : η → Type*}
id ┴
typ ┴
407 {f : Π j : η, ιs j → M}
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
408 (hindep : ∀j, linear_independent R (f j))
id ┴ └────────────────┘ ┴ ┴ ┴
src └────────────────┘
typ ┴ └────────────────┘ ┴ ┴ ┴
doc └────────────────┘
409 (hd : ∀i, ∀t:set η, finite t → i ∉ t →
id ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └─┘ └────┘ ┴
typ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────┘
410 disjoint (span R (range (f i))) (⨆i∈t, span R (range (f i)))) :
id └──────┘ └──┘ ┴ └───┘ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ └───┘ ┴ ┴
src └──────┘ └──┘ └───┘ ┴ ┴ └──┘ └───┘
typ └──────┘ └──┘ ┴ └───┘ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ └───┘ ┴ ┴
doc └──────┘ └──┘ └───┘ ┴ ┴ └──┘ └───┘
411 linear_independent R (λ ji : Σ j, ιs j, f ji.1 ji.2) :=
id └────────────────┘ ┴ ┴ ┴┴ └┘ ┴ ┴ └┘┴ └┘┴
src └────────────────┘ ┴ ┴ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴┴ └┘ ┴ ┴ └┘┴ └┘┴
doc └────────────────┘
412 begin
st └─────
413 by_cases zero_eq_one : (0 : R) = 1,
id ┴ ┴
src └───────┘ └─┘ └──┘ └┘┴└┘
typ └───────┘ └─┘ └──┘┴└┘┴└┘
doc └───────┘ └─┘ └──┘ └┘ └┘
txt └───────┘ └─┘ └──┘ └┘ └┘
par └───────┘ └─┘ └──┘ └┘ └┘
pid ┴ └─┘ └──┘ └┘ ┴┴
st ───────────────────────────────────┘
414 { apply linear_independent_of_zero_eq_one zero_eq_one },
st ┴
415 apply linear_independent.of_subtype_range,
416 { rintros ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy,
417 by_cases h_cases : x₁ = y₁,
418 subst h_cases,
419 { apply sigma.eq,
420 rw linear_independent.injective zero_eq_one (hindep _) hxy,
421 refl },
st ┴
422 { have h0 : f x₁ x₂ = 0,
423 { apply disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁)
424 (λ h, h_cases (eq_of_mem_singleton h))) (f x₁ x₂) (subset_span (mem_range_self _)),
425 rw supr_singleton,
426 simp only [] at hxy,
427 rw hxy,
428 exact (subset_span (mem_range_self y₂)) },
st ┴
429 exact false.elim (ne_zero_of_linear_independent zero_eq_one (hindep x₁) h0) } },
st └─┘
430 rw range_sigma_eq_Union_range,
431 apply linear_independent_Union_finite_subtype (λ j, (hindep j).to_subtype_range) hd,
st └─
432 end
st ──┘
433
434 end subtype
435
436 section repr
437 variables (hv : linear_independent R v)
id └────────────────┘
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
438
439 /-- Canonical isomorphism between linear combinations and the span of linearly independent vectors. -/
440 def linear_independent.total_equiv (hv : linear_independent R v) : (ι →₀ R) ≃ₗ[R] span R (range v) :=
id └────────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘┴┴ └──┘ ┴ └───┘ ┴
src └────────────────┘ └┘ └─┘ ┴ └──┘ └───┘
typ └────────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘┴┴ └──┘ ┴ └───┘ ┴
doc └────────────────┘ └┘ └─┘ ┴ └──┘ └───┘
441 begin
st └───┘
442 apply linear_equiv.of_bijective (linear_map.cod_restrict (span R (range v)) (finsupp.total ι M R v) _),
443 { rw linear_map.ker_cod_restrict,
444 apply hv },
st └┘
445 { rw [linear_map.range, linear_map.map_cod_restrict, ← linear_map.range_le_iff_comap,
446 range_subtype, map_top],
447 rw finsupp.range_total,
448 apply le_refl (span R (range v)) },
id ┴ ┴
typ ┴ ┴
st └┘
449 { intro l,
450 rw ← finsupp.range_total,
451 rw linear_map.mem_range,
452 apply mem_range_self l }
st └─
453 end
st ──┘
454
455 /-- Linear combination representing a vector in the span of linearly independent vectors.
456
457 Given a family of linearly independent vectors, we can represent any vector in their span as
458 a linear combination of these vectors. These are provided by this linear map.
459 It is simply one direction of `linear_independent.total_equiv` -/
460 def linear_independent.repr (hv : linear_independent R v) :
id ┴ ┴
typ ┴ ┴
461 span R (range v) →ₗ[R] ι →₀ R := hv.total_equiv.symm
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
462
463 lemma linear_independent.total_repr (x) : finsupp.total ι M R v (hv.repr x) = x :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
464 subtype.coe_ext.1 (linear_equiv.apply_symm_apply hv.total_equiv x)
465
466 lemma linear_independent.total_comp_repr : (finsupp.total ι M R v).comp hv.repr = submodule.subtype _ :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
467 linear_map.ext $ hv.total_repr
468
469 lemma linear_independent.repr_ker : hv.repr.ker = ⊥ :=
470 by rw [linear_independent.repr, linear_equiv.ker]
471
472 lemma linear_independent.repr_range : hv.repr.range = ⊤ :=
473 by rw [linear_independent.repr, linear_equiv.range]
474
475 lemma linear_independent.repr_eq
476 {l : ι →₀ R} {x} (eq : finsupp.total ι M R v l = ↑x) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
477 hv.repr x = l :=
478 begin
479 have : ↑((linear_independent.total_equiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l)
480 = finsupp.total ι M R v l := rfl,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
481 have : (linear_independent.total_equiv hv : (ι →₀ R) →ₗ[R] span R (range v)) l = x,
id ┴ ┴ ┴
typ ┴ ┴ ┴
482 { rw eq at this,
483 exact subtype.coe_ext.2 this },
st └┘
484 rw ←linear_equiv.symm_apply_apply hv.total_equiv l,
485 rw ←this,
486 refl,
487 end
st └─┘
488
489 lemma linear_independent.repr_eq_single (i) (x) (hx : ↑x = v i) :
id ┴ ┴
typ ┴ ┴
490 hv.repr x = finsupp.single i 1 :=
id ┴
typ ┴
491 begin
492 apply hv.repr_eq,
493 simp [finsupp.total_single, hx]
494 end
st └─┘
495
496 lemma linear_independent_iff_not_smul_mem_span :
497 linear_independent R v ↔ (∀ (i : ι) (a : R), a • (v i) ∈ span R (v '' (univ \ {i})) → a = 0) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
498 ⟨ λ hv i a ha, begin
id ┴ ┴
typ ┴ ┴
499 rw [finsupp.span_eq_map_total, mem_map] at ha,
500 rcases ha with ⟨l, hl, e⟩,
501 rw sub_eq_zero.1 (linear_independent_iff.1 hv (l - finsupp.single i a) (by simp [e])) at hl,
id ┴ ┴
typ ┴ ┴
502 by_contra hn,
503 exact (not_mem_of_mem_diff (hl $ by simp [hn])) (mem_singleton _),
504 end, λ H, linear_independent_iff.2 $ λ l hl, begin
st └─┘
505 ext i, simp,
506 by_contra hn,
507 refine hn (H i _ _),
id ┴
typ ┴
508 refine (finsupp.mem_span_iff_total _).2 ⟨finsupp.single i (l i) - l, _, _⟩,
id ┴
typ ┴
509 { rw finsupp.mem_supported',
510 intros j hj,
511 have hij : j = i :=
id ┴ ┴
typ ┴ ┴
512 classical.not_not.1
513 (λ hij : j ≠ i, hj ((mem_diff _).2 ⟨mem_univ _, λ h, hij (eq_of_mem_singleton h)⟩)),
id ┴ ┴
typ ┴ ┴
514 simp [hij] },
id └─┘
typ └─┘
st └┘
515 { simp [hl] }
st └─
516 end⟩
st ──┘
517
518 end repr
519
520 lemma surjective_of_linear_independent_of_span
521 (hv : linear_independent R v) (f : ι' ↪ ι)
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
522 (hss : range v ⊆ span R (range (v ∘ f))) (zero_ne_one : 0 ≠ (1 : R)):
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
523 surjective f :=
id ┴
typ ┴
524 begin
525 intros i,
526 let repr : (span R (range (v ∘ f)) : Type*) → ι' →₀ R := (hv.comp f f.inj).repr,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
527 let l := (repr ⟨v i, hss (mem_range_self i)⟩).map_domain f,
id ┴ ┴ ┴
typ ┴ ┴ ┴
528 have h_total_l : finsupp.total ι M R v l = v i,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
529 { dsimp only [l],
530 rw finsupp.total_map_domain,
531 rw (hv.comp f f.inj).total_repr,
532 { refl },
st └┘
533 { exact f.inj } },
st └──┘
534 have h_total_eq : (finsupp.total ι M R v) l = (finsupp.total ι M R v) (finsupp.single i 1),
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
535 by rw [h_total_l, finsupp.total_single, one_smul],
st ┴
536 have l_eq : l = _ := linear_map.ker_eq_bot.1 hv h_total_eq,
537 dsimp only [l] at l_eq,
538 rw ←finsupp.emb_domain_eq_map_domain at l_eq,
539 rcases finsupp.single_of_emb_domain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with ⟨i', hi'⟩,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
540 use i',
id └┘
typ └┘
541 exact hi'.2
542 end
st └─┘
543
544 lemma eq_of_linear_independent_of_span_subtype {s t : set M} (zero_ne_one : (0 : R) ≠ 1)
id ┴ ┴
typ ┴ ┴
545 (hs : linear_independent R (λ x, x : s → M)) (h : t ⊆ s) (hst : s ⊆ span R t) : s = t :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
546 begin
547 let f : t ↪ s := ⟨λ x, ⟨x.1, h x.2⟩, λ a b hab, subtype.val_injective (subtype.mk.inj hab)⟩,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
548 have h_surj : surjective f,
549 { apply surjective_of_linear_independent_of_span hs f _ zero_ne_one,
550 convert hst; simp [f, comp], },
st └┘
551 show s = t,
id ┴ ┴
typ ┴ ┴
552 { apply subset.antisymm _ h,
553 intros x hx,
554 rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩,
id ┴
typ ┴
555 convert y.mem,
556 rw ← subtype.mk.inj hy,
557 refl }
st └─
558 end
st ──┘
559
560 open linear_map
561
562 lemma linear_independent.image (hv : linear_independent R v) {f : M →ₗ M'}
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
563 (hf_inj : disjoint (span R (range v)) f.ker) : linear_independent R (f ∘ v) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
564 begin
565 rw [disjoint, ← set.image_univ, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
566 map_le_iff_le_comap, comap_bot, finsupp.supported_univ, top_inf_eq] at hf_inj,
567 unfold linear_independent at hv,
568 rw hv at hf_inj,
569 haveI : inhabited M := ⟨0⟩,
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
570 rw [linear_independent, finsupp.total_comp],
571 rw [@finsupp.lmap_domain_total _ _ R _ _ _ _ _ _ _ _ _ _ f, ker_comp, eq_bot_iff],
id ┴
typ ┴
572 apply hf_inj,
573 exact λ _, rfl,
id ┴
typ ┴
574 end
st └─┘
575
576 lemma linear_independent.image_subtype {s : set M} {f : M →ₗ M'} (hs : linear_independent R (λ x, x : s → M))
id └┘ ┴ ┴ └┘ ┴ ┴
src └┘
typ └┘ ┴ ┴ └┘ ┴ ┴
577 (hf_inj : disjoint (span R s) f.ker) : linear_independent R (λ x, x : f '' s → M') :=
id ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
578 begin
579 rw [disjoint, ← set.image_id s, finsupp.span_eq_map_total, map_inf_eq_map_inf_comap,
580 map_le_iff_le_comap, comap_bot] at hf_inj,
581 haveI : inhabited M := ⟨0⟩,
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
582 rw [linear_independent_subtype_disjoint, disjoint, ← finsupp.lmap_domain_supported _ _ f, map_inf_eq_map_inf_comap,
583 map_le_iff_le_comap, ← ker_comp],
584 rw [@finsupp.lmap_domain_total _ _ R _ _ _, ker_comp],
id ┴
typ ┴
585 { exact le_trans (le_inf inf_le_left hf_inj) (le_trans (linear_independent_subtype_disjoint.1 hs) bot_le) },
st └┘
586 { simp }
st └─
587 end
st ──┘
588
589 lemma linear_independent_inl_union_inr {s : set M} {t : set M'}
id └┘ ┴ └┘ └┘
src └┘ └┘
typ └┘ ┴ └┘ └┘
590 (hs : linear_independent R (λ x, x : s → M))
id ┴ ┴
typ ┴ ┴
591 (ht : linear_independent R (λ x, x : t → M')) :
id ┴ └┘
typ ┴ └┘
592 linear_independent R (λ x, x : inl R M M' '' s ∪ inr R M M' '' t → M × M') :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
593 begin
594 apply linear_independent_union,
595 exact (hs.image_subtype $ by simp),
596 exact (ht.image_subtype $ by simp),
597 rw [span_image, span_image];
598 simp [disjoint_iff, prod_inf_prod]
599 end
st └─┘
600
601 lemma linear_independent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
602 (hv : linear_independent R v) (hv' : linear_independent R v') :
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
603 linear_independent R (sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
604 begin
605 by_cases zero_eq_one : (0 : R) = 1,
606 { apply linear_independent_of_zero_eq_one zero_eq_one },
st └┘
607 have inj_v : injective v := (linear_independent.injective zero_eq_one hv),
id ┴
typ ┴
608 have inj_v' : injective v' := (linear_independent.injective zero_eq_one hv'),
id └┘
typ └┘
609 apply linear_independent.of_subtype_range,
610 { apply sum.elim_injective,
611 { exact injective_comp prod.injective_inl inj_v },
id └───┘
typ └───┘
st └┘
612 { exact injective_comp prod.injective_inr inj_v' },
id └────┘
typ └────┘
st └┘
613 { intros, simp [ne_zero_of_linear_independent zero_eq_one hv] } },
st └──┘
614 { rw sum.elim_range,
615 apply linear_independent_union,
616 { apply linear_independent.to_subtype_range,
617 apply linear_independent.image hv,
618 simp [ker_inl] },
st └┘
619 { apply linear_independent.to_subtype_range,
620 apply linear_independent.image hv',
621 simp [ker_inr] },
st └┘
622 { apply disjoint_mono _ _ disjoint_inl_inr,
623 { rw [set.range_comp, span_image],
624 apply linear_map.map_le_range },
st └┘
625 { rw [set.range_comp, span_image],
626 apply linear_map.map_le_range } } }
st └─────
627 end
st ──┘
628
629 /-- Dedekind's linear independence of characters -/
630 -- See, for example, Keith Conrad's note <https://kconrad.math.uconn.edu/blurbs/galoistheory/linearchar.pdf>
631 theorem linear_independent_monoid_hom (G : Type*) [monoid G] (L : Type*) [integral_domain L] :
id └──┘ ┴ └──┘ └──┘ └─┘ ┴
src └──┘ └──┘ └──┘ └─┘
typ └──┘ ┴ └──┘ └──┘ └─┘ ┴
632 @linear_independent _ L (G → L) (λ f, f : (G →* L) → (G → L)) _ _ _ :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
633 by letI := classical.dec_eq (G →* L);
id ┴ ┴
typ ┴ ┴
634 letI : mul_action L L := distrib_mul_action.to_mul_action L L;
id ┴ ┴
typ ┴ ┴
635 -- We prove linear independence by showing that only the trivial linear combination vanishes.
636 exact linear_independent_iff'.2
637 -- To do this, we use `finset` induction,
638 (λ s, finset.induction_on s (λ g hg i, false.elim) $ λ a s has ih g hg,
639 -- Here
640 -- * `a` is a new character we will insert into the `finset` of characters `s`,
641 -- * `ih` is the fact that only the trivial linear combination of characters in `s` is zero
642 -- * `hg` is the fact that `g` are the coefficients of a linear combination summing to zero
643 -- and it remains to prove that `g` vanishes on `insert a s`.
644
645 -- We now make the key calculation:
646 -- For any character `i` in the original `finset`, we have `g i • i = g i • a` as functions on the monoid `G`.
647 have h1 : ∀ i ∈ s, (g i • i : G → L) = g i • a, from λ i his, funext $ λ x : G,
648 -- We prove these expressions are equal by showing
649 -- the differences of their values on each monoid element `x` is zero
650 eq_of_sub_eq_zero $ ih (λ j, g j * j x - g j * a x)
651 (funext $ λ y : G, calc
652 -- After that, it's just a chase scene.
653 s.sum (λ i, ((g i * i x - g i * a x) • i : G → L)) y
654 = s.sum (λ i, (g i * i x - g i * a x) * i y) : pi.finset_sum_apply _ _ _
655 ... = s.sum (λ i, g i * i x * i y - g i * a x * i y) : finset.sum_congr rfl
656 (λ _ _, sub_mul _ _ _)
657 ... = s.sum (λ i, g i * i x * i y) - s.sum (λ i, g i * a x * i y) : finset.sum_sub_distrib
658 ... = (g a * a x * a y + s.sum (λ i, g i * i x * i y))
659 - (g a * a x * a y + s.sum (λ i, g i * a x * i y)) : by rw add_sub_add_left_eq_sub
660 ... = (insert a s).sum (λ i, g i * i x * i y) - (insert a s).sum (λ i, g i * a x * i y) :
661 by rw [finset.sum_insert has, finset.sum_insert has]
st ┴
662 ... = (insert a s).sum (λ i, g i * i (x * y)) - (insert a s).sum (λ i, a x * (g i * i y)) :
663 congr (congr_arg has_sub.sub (finset.sum_congr rfl $ λ i _, by rw [i.map_mul, mul_assoc]))
st ┴
664 (finset.sum_congr rfl $ λ _ _, by rw [mul_assoc, mul_left_comm])
st ┴
665 ... = (insert a s).sum (λ i, (g i • i : G → L)) (x * y)
666 - a x * (insert a s).sum (λ i, (g i • i : G → L)) y :
667 by rw [pi.finset_sum_apply, pi.finset_sum_apply, finset.mul_sum]; refl
668 ... = 0 - a x * 0 : by rw hg; refl
669 ... = 0 : by rw [mul_zero, sub_zero])
st ┴
670 i
671 his,
672 -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
673 -- there is some element of the monoid on which it differs from `a`.
674 have h2 : ∀ i : G →* L, i ∈ s → ∃ y, i y ≠ a y, from λ i his,
id ┴
typ ┴
675 classical.by_contradiction $ λ h,
676 have hia : i = a, from monoid_hom.ext $ λ y, classical.by_contradiction $ λ hy, h ⟨y, hy⟩,
id ┴
typ ┴
677 has $ hia ▸ his,
678 -- From these two facts we deduce that `g` actually vanishes on `s`,
679 have h3 : ∀ i ∈ s, g i = 0, from λ i his, let ⟨y, hy⟩ := h2 i his in
id ┴
typ ┴
680 have h : g i • i y = g i • a y, from congr_fun (h1 i his) y,
681 or.resolve_right (mul_eq_zero.1 $ by rw [mul_sub, sub_eq_zero]; exact h) (sub_ne_zero_of_ne hy),
682 -- And so, using the fact that the linear combination over `s` and over `insert a s` both vanish,
683 -- we deduce that `g a = 0`.
684 have h4 : g a = 0, from calc
685 g a = g a * 1 : (mul_one _).symm
686 ... = (g a • a : G → L) 1 : by rw ← a.map_one; refl
id └──┘
src └──┘
typ └──┘
doc └──┘
687 ... = (insert a s).sum (λ i, (g i • i : G → L)) 1 : begin
688 rw finset.sum_eq_single a,
689 { intros i his hia, rw finset.mem_insert at his, rw [h3 i (his.resolve_left hia), zero_smul] },
st ┴ └┘
690 { intros haas, exfalso, apply haas, exact finset.mem_insert_self a s }
st └┘
691 end
st └─┘
692 ... = 0 : by rw hg; refl,
693 -- Now we're done; the last two facts together imply that `g` vanishes on every element of `insert a s`.
694 (finset.forall_mem_insert _ _ _).2 ⟨h4, h3⟩)
695
696 lemma le_of_span_le_span {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
id ┴ ┴
typ ┴ ┴
697 (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u)
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
698 (hst : span R s ≤ span R t) : s ⊆ t :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
699 begin
700 have := eq_of_linear_independent_of_span_subtype zero_ne_one
701 (hl.mono (set.union_subset hsu htu))
702 (set.subset_union_right _ _)
703 (set.union_subset (set.subset.trans subset_span hst) subset_span),
704 rw ← this, apply set.subset_union_left
705 end
st └─┘
706
707 lemma span_le_span_iff {s t u: set M} (zero_ne_one : (0 : R) ≠ 1)
id ┴ ┴
typ ┴ ┴
708 (hl : linear_independent R (subtype.val : u → M )) (hsu : s ⊆ u) (htu : t ⊆ u) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
709 span R s ≤ span R t ↔ s ⊆ t :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
710 ⟨le_of_span_le_span zero_ne_one hl hsu htu, span_mono⟩
711
712 variables (R) (v)
713 /-- A family of vectors is a basis if it is linearly independent and all vectors are in the span. -/
714 def is_basis := linear_independent R v ∧ span R (range v) = ⊤
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
715 variables {R} {v}
716
717 section is_basis
718 variables {s t : set M} (hv : is_basis R v)
719
720 lemma is_basis.mem_span (hv : is_basis R v) : ∀ x, x ∈ span R (range v) := eq_top_iff'.1 hv.2
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
721
722 lemma is_basis.comp (hv : is_basis R v) (f : ι' → ι) (hf : bijective f) :
id ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴
723 is_basis R (v ∘ f) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
724 begin
725 split,
726 { apply hv.1.comp f hf.1 },
st └┘
727 { rw[set.range_comp, range_iff_surjective.2 hf.2, image_univ, hv.2] }
id └┘
typ └┘
st ┴ └─
728 end
st ──┘
729
730 lemma is_basis.injective (hv : is_basis R v) (zero_ne_one : (0 : R) ≠ 1) : injective v :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
731 λ x y h, linear_independent.injective zero_ne_one hv.1 h
id ┴ ┴
typ ┴ ┴
732
733 /- Given a basis, any vector can be written as a linear combination of the basis vectors. They are
734 given by this linear map. This is one direction of `module_equiv_finsupp` -/
735 def is_basis.repr : M →ₗ (ι →₀ R) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
736 (hv.1.repr).comp (linear_map.id.cod_restrict _ hv.mem_span)
737
738 lemma is_basis.total_repr (x) : finsupp.total ι M R v (hv.repr x) = x :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
739 hv.1.total_repr ⟨x, _⟩
id ┴
typ ┴
740
741 lemma is_basis.total_comp_repr : (finsupp.total ι M R v).comp hv.repr = linear_map.id :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
742 linear_map.ext hv.total_repr
743
744 lemma is_basis.repr_ker : hv.repr.ker = ⊥ :=
745 linear_map.ker_eq_bot.2 $ injective_of_left_inverse hv.total_repr
746
747 lemma is_basis.repr_range : hv.repr.range = finsupp.supported R R univ :=
id ┴ ┴
typ ┴ ┴
748 by rw [is_basis.repr, linear_map.range, submodule.map_comp,
749 linear_map.map_cod_restrict, submodule.map_id, comap_top, map_top, hv.1.repr_range,
750 finsupp.supported_univ]
st ┴
751
752 lemma is_basis.repr_total (x : ι →₀ R) (hx : x ∈ finsupp.supported R R (univ : set ι)) :
id ┴ ┴ ┴ ┴ └┘ ┴
src └┘
typ ┴ ┴ ┴ ┴ └┘ ┴
753 hv.repr (finsupp.total ι M R v x) = x :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
754 begin
755 rw [← hv.repr_range, linear_map.mem_range] at hx,
756 cases hx with w hw,
757 rw [← hw, hv.total_repr],
st ┴
758 end
st └─┘
759
760 lemma is_basis.repr_eq_single {i} : hv.repr (v i) = finsupp.single i 1 :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
761 by apply hv.1.repr_eq_single; simp
762
763 /-- Construct a linear map given the value at the basis. -/
764 def is_basis.constr (f : ι → M') : M →ₗ[R] M' :=
id ┴ └┘ ┴ ┴ └┘
typ ┴ └┘ ┴ ┴ └┘
765 (finsupp.total M' M' R id).comp $ (finsupp.lmap_domain R R f).comp hv.repr
id └┘ └┘ ┴ ┴ ┴ ┴
typ └┘ └┘ ┴ ┴ ┴ ┴
766
767 theorem is_basis.constr_apply (f : ι → M') (x : M) :
id ┴ └┘ ┴
typ ┴ └┘ ┴
768 (hv.constr f : M → M') x = (hv.repr x).sum (λb a, a • f b) :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
769 by dsimp [is_basis.constr];
770 rw [finsupp.total_apply, finsupp.sum_map_domain_index]; simp [add_smul]
771
772 lemma is_basis.ext {f g : M →ₗ[R] M'} (hv : is_basis R v) (h : ∀i, f (v i) = g (v i)) : f = g :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
773 begin
774 apply linear_map.ext (λ x, linear_eq_on (range v) _ (hv.mem_span x)),
775 exact (λ y hy, exists.elim (set.mem_range.1 hy) (λ i hi, by rw ←hi; exact h i))
id ┴ ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴
776 end
st └─┘
777
778 lemma constr_basis {f : ι → M'} {i : ι} (hv : is_basis R v) :
id ┴ └┘ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴
779 (hv.constr f : M → M') (v i) = f i :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴
780 by simp [is_basis.constr_apply, hv.repr_eq_single, finsupp.sum_single_index]
781
782 lemma constr_eq {g : ι → M'} {f : M →ₗ[R] M'} (hv : is_basis R v)
id ┴ └┘ ┴ ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴
783 (h : ∀i, g i = f (v i)) : hv.constr g = f :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
784 hv.ext $ λ i, (constr_basis hv).trans (h i)
id ┴ ┴
typ ┴ ┴
785
786 lemma constr_self (f : M →ₗ[R] M') : hv.constr (λ i, f (v i)) = f :=
id ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
787 constr_eq hv $ λ x, rfl
id ┴
typ ┴
788
789 lemma constr_zero (hv : is_basis R v) : hv.constr (λi, (0 : M')) = 0 :=
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
790 constr_eq hv $ λ x, rfl
id ┴
typ ┴
791
792 lemma constr_add {g f : ι → M'} (hv : is_basis R v) :
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
793 hv.constr (λi, f i + g i) = hv.constr f + hv.constr g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
794 constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id └┘
src └┘
typ └┘
795
796 lemma constr_neg {f : ι → M'} (hv : is_basis R v) : hv.constr (λi, - f i) = - hv.constr f :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
797 constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id └┘
src └┘
typ └┘
798
799 lemma constr_sub {g f : ι → M'} (hs : is_basis R v) :
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
800 hv.constr (λi, f i - g i) = hs.constr f - hs.constr g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
801 by simp [constr_add, constr_neg]
802
803 -- this only works on functions if `R` is a commutative ring
804 lemma constr_smul {ι R M M'} [comm_ring R]
id └──┘ └─┘ ┴
src └──┘ └─┘
typ └──┘ └─┘ ┴
805 [add_comm_group M] [add_comm_group M'] [module R M] [module R M']
id └┘ └┘ └┘ └┘ ┴ ┴ └──┘ └──┘ ┴ └┘ ┴ ┴ ┴ └┘
src └┘ └┘ └┘ └┘ ┴ └──┘ └──┘ ┴
typ └┘ └┘ └┘ └┘ ┴ ┴ └──┘ └──┘ ┴ └┘ ┴ ┴ ┴ └┘
806 {v : ι → R} {f : ι → M'} {a : R} (hv : is_basis R v) {b : M} :
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
807 hv.constr (λb, a • f b) = a • hv.constr f :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
808 constr_eq hv $ by simp [constr_basis hv] {contextual := tt}
id └┘
src └┘
typ └┘
809
810 lemma constr_range [inhabited ι] (hv : is_basis R v) {f : ι → M'} :
id └──┘ └─┘ ┴ ┴ ┴ ┴ └┘
src └──┘ └─┘
typ └──┘ └─┘ ┴ ┴ ┴ ┴ └┘
811 (hv.constr f).range = span R (range f) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
812 by rw [is_basis.constr, linear_map.range_comp, linear_map.range_comp, is_basis.repr_range,
813 finsupp.lmap_domain_supported, ←set.image_univ, ←finsupp.span_eq_map_total, image_id]
st ┴
814
815 /-- Canonical equivalence between a module and the linear combinations of basis vectors. -/
816 def module_equiv_finsupp (hv : is_basis R v) : M ≃ₗ[R] ι →₀ R :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
817 (hv.1.total_equiv.trans (linear_equiv.of_top _ hv.2)).symm
818
819 /-- Isomorphism between the two modules, given two modules M and M' with respective bases v and v'
820 and a bijection between the two bases. -/
821 def equiv_of_is_basis {v : ι → M} {v' : ι' → M'} {f : M → M'} {g : M' → M}
id ┴ ┴ └┘ ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ ┴ ┴ └┘ └┘
822 (hv : is_basis R v) (hv' : is_basis R v') (hf : ∀i, f (v i) ∈ range v') (hg : ∀i, g (v' i) ∈ range v)
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
823 (hgf : ∀i, g (f (v i)) = v i) (hfg : ∀i, f (g (v' i)) = v' i) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
824 M ≃ₗ M' :=
id ┴ └┘
typ ┴ └┘
825 { inv_fun := hv'.constr (g ∘ v'),
id ┴ ┴
typ ┴ ┴
826 left_inv :=
827 have (hv'.constr (g ∘ v')).comp (hv.constr (f ∘ v)) = linear_map.id,
id ┴ ┴ ┴
typ ┴ ┴ ┴
828 from hv.ext $ λ i, exists.elim (hf i) (λ i' hi', by simp [constr_basis, hi'.symm]; rw [hi', hgf]),
id ┴ ┴ └┘
typ ┴ ┴ └┘
st ┴
829 λ x, congr_arg (λ h:M →ₗ[R] M, h x) this,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
830 right_inv :=
831 have (hv.constr (f ∘ v)).comp (hv'.constr (g ∘ v')) = linear_map.id,
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
832 from hv'.ext $ λ i', exists.elim (hg i') (λ i hi, by simp [constr_basis, hi.symm]; rw [hi, hfg]),
id └┘ └┘ ┴
typ └┘ └┘ ┴
st ┴
833 λ y, congr_arg (λ h:M' →ₗ[R] M', h y) this,
id ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴
834 ..hv.constr (f ∘ v) }
id ┴ ┴
typ ┴ ┴
835
836 lemma is_basis_inl_union_inr {v : ι → M} {v' : ι' → M'}
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
837 (hv : is_basis R v) (hv' : is_basis R v') : is_basis R (sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘
838 begin
839 split,
840 apply linear_independent_inl_union_inr' hv.1 hv'.1,
841 rw [sum.elim_range, span_union,
842 set.range_comp, span_image (inl R M M'), hv.2, map_top,
id ┴ ┴ └┘
typ ┴ ┴ └┘
843 set.range_comp, span_image (inr R M M'), hv'.2, map_top],
id ┴ ┴ └┘
typ ┴ ┴ └┘
844 exact linear_map.sup_range_inl_inr
845 end
st └─┘
846
847 end is_basis
848
849 lemma is_basis_singleton_one (R : Type*) [unique ι] [ring R] :
id └┘ └┘ ┴ └─┘ ┴
src └┘ └┘ └─┘
typ └┘ └┘ ┴ └─┘ ┴
850 is_basis R (λ (_ : ι), (1 : R)) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
851 begin
852 split,
853 { refine linear_independent_iff.2 (λ l, _),
854 rw [finsupp.unique_single l, finsupp.total_single, smul_eq_mul, mul_one],
855 intro hi,
856 simp [hi] },
st └┘
857 { refine top_unique (λ _ _, _),
id ┴
typ ┴
858 simp [submodule.mem_span_singleton] }
st └─
859 end
st ──┘
860
861 protected lemma linear_equiv.is_basis (hs : is_basis R v)
id ┴ ┴
typ ┴ ┴
862 (f : M ≃ₗ[R] M') : is_basis R (f ∘ v) :=
id ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴
863 begin
864 split,
865 { apply @linear_independent.image _ _ _ _ _ _ _ _ _ _ hs.1 (f : M →ₗ[R] M'),
866 simp [linear_equiv.ker f] },
st └┘
867 { rw set.range_comp,
868 have : span R ((f : M →ₗ[R] M') '' range v) = ⊤,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
869 { rw [span_image (f : M →ₗ[R] M'), hs.2],
id ┴ ┴ └┘
typ ┴ ┴ └┘
870 simp },
st └┘
871 exact this }
st └─
872 end
st ──┘
873
874 lemma is_basis_span (hs : linear_independent R v) :
id ┴ ┴
typ ┴ ┴
875 @is_basis ι R (span R (range v)) (λ i : ι, ⟨v i, subset_span (mem_range_self _)⟩) _ _ _ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
876 begin
877 split,
878 { apply linear_independent_span hs },
st └┘
879 { rw eq_top_iff',
880 intro x,
881 have h₁ : subtype.val '' set.range (λ i, subtype.mk (v i) _) = range v,
id ┴ ┴
typ ┴ ┴
882 by rw ←set.range_comp,
883 have h₂ : map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _)))
id ┴
typ ┴
884 = span R (range v),
id ┴ ┴
typ ┴ ┴
885 by rw [←span_image, submodule.subtype_eq_val, h₁],
st ┴
886 have h₃ : (x : M) ∈ map (submodule.subtype _) (span R (set.range (λ i, subtype.mk (v i) _))),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
887 by rw h₂; apply subtype.mem x,
888 rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩,
889 have h_x_eq_y : x = y,
890 by rw [subtype.coe_ext, ← hy₂]; simp,
891 rw h_x_eq_y,
892 exact hy₁ }
st └─
893 end
st ──┘
894
895 lemma is_basis_empty (h_empty : ¬ nonempty ι) (h : ∀x:M, x = 0) : is_basis R (λ x : ι, (0 : M)) :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
896 ⟨ linear_independent_empty_type h_empty,
id └┘ └┘
typ └┘ └┘
897 eq_top_iff'.2 $ assume x, (h x).symm ▸ submodule.zero_mem _ ⟩
id ┴ ┴
typ ┴ ┴
898
899 lemma is_basis_empty_bot (h_empty : ¬ nonempty ι) : is_basis R (λ _ : ι, (0 : (⊥ : submodule R M))) :=
id ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ └┘
typ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴
900 begin
901 apply is_basis_empty h_empty,
902 intro x,
903 apply subtype.ext.2,
904 exact (submodule.mem_bot R).1 (subtype.mem x),
id ┴
typ ┴
905 end
st └─┘
906
907 open fintype
908 variables [fintype ι] (h : is_basis R v)
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
doc └──┘ ┴
909
910 /-- A module over R with a finite basis is linearly equivalent to functions from its basis to R. -/
911 def equiv_fun_basis : M ≃ₗ[R] (ι → R) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
912 linear_equiv.trans (module_equiv_finsupp h)
913 { to_fun := finsupp.to_fun,
914 add := λ x y, by ext; exact finsupp.add_apply,
915 smul := λ x y, by ext; exact finsupp.smul_apply,
id ┴
typ ┴
916 ..finsupp.equiv_fun_on_fintype }
917
918 theorem module.card_fintype [fintype R] [fintype M] :
id └──┘ ┴ ┴ └┘ └┘ ┴ ┴
src └──┘ ┴ └┘ └┘ ┴
typ └──┘ ┴ ┴ └┘ └┘ ┴ ┴
doc └──┘ ┴ └┘ └┘ ┴
919 card M = (card R) ^ (card ι) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
920 calc card M = card (ι → R) : card_congr (equiv_fun_basis h).to_equiv
id ┴ ┴ ┴
typ ┴ ┴ ┴
921 ... = card R ^ card ι : card_fun
id ┴ ┴
typ ┴ ┴
922
923 /-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
924 a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
925 @[simp] lemma equiv_fun_basis_symm_apply (x : ι → R) :
id ┴ ┴
typ ┴ ┴
doc └──┘
926 (equiv_fun_basis h).symm x = finset.sum finset.univ (λi, x i • v i) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
927 begin
928 change finsupp.sum
929 ((finsupp.equiv_fun_on_fintype.symm : (ι → R) ≃ (ι →₀ R)) x) (λ (i : ι) (a : R), a • v i)
930 = finset.sum finset.univ (λi, x i • v i),
931 dsimp [finsupp.equiv_fun_on_fintype, finsupp.sum],
932 rw finset.sum_filter,
933 refine finset.sum_congr rfl (λi hi, _),
id ┴
typ ┴
934 by_cases H : x i = 0,
id ┴ ┴
typ ┴ ┴
935 { simp [H] },
st └┘
936 { simp [H], refl }
st └─
937 end
st ──┘
938
939 end module
940
941 section vector_space
942 variables
943 {v : ι → V}
944 [discrete_field K] [add_comm_group V] [add_comm_group V']
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
945 [vector_space K V] [vector_space K V']
946 {s t : set V} {x y z : V}
947 include K
948 open submodule
949
950 /- TODO: some of the following proofs can generalized with a zero_ne_one predicate type class
951 (instead of a data containing type class) -/
952
953 section
954 set_option class.instance_max_depth 36
doc └──────────────────────┘
955
956 lemma mem_span_insert_exchange : x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
957 begin
958 simp [mem_span_insert],
959 rintro a z hz rfl h,
960 refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, _⟩,
id ┴ ┴
typ ┴ ┴
961 have a0 : a ≠ 0, {rintro rfl, simp * at *},
id ┴
typ ┴
st └┘
962 simp [a0, smul_add, smul_smul]
963 end
st └─┘
964
965 end
966
967 lemma linear_independent_iff_not_mem_span : linear_independent K v ↔ (∀i, v i ∉ span K (v '' (univ \ {i}))) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
968 begin
969 apply linear_independent_iff_not_smul_mem_span.trans,
970 split,
971 { intros h i h_in_span,
972 apply one_ne_zero (h i 1 (by simp [h_in_span])) },
id ┴
typ ┴
st └┘
973 { intros h i a ha,
974 by_contradiction ha',
975 exact false.elim (h _ ((smul_mem_iff _ ha').1 ha)) }
st └─
976 end
st ──┘
977
978 lemma linear_independent_unique [unique ι] (h : v (default ι) ≠ 0): linear_independent K v :=
id └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴
979 begin
980 rw linear_independent_iff,
981 intros l hl,
982 ext i,
983 rw [unique.eq_default i, finsupp.zero_apply],
id ┴
typ ┴
984 by_contra hc,
985 have := smul_smul (l (default ι))⁻¹ (l (default ι)) (v (default ι)),
id ┴ ┴
typ ┴ ┴
986 rw [finsupp.unique_single l, finsupp.total_single] at hl,
987 rw [hl, inv_mul_cancel hc, smul_zero, one_smul] at this,
988 exact h this.symm
989 end
st └─┘
990
991 lemma linear_independent_singleton {x : V} (hx : x ≠ 0) : linear_independent K (λ x, x : ({x} : set V) → V) :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
992 begin
993 apply @linear_independent_unique _ _ _ _ _ _ _ _ _,
994 apply set.unique_singleton,
995 apply hx,
996 end
st └─┘
997
998 lemma disjoint_span_singleton {p : submodule K V} {x : V} (x0 : x ≠ 0) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
999 disjoint p (span K {x}) ↔ x ∉ p :=
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
1000 ⟨λ H xp, x0 (disjoint_def.1 H _ xp (singleton_subset_iff.1 subset_span:_)),
1001 begin
1002 simp [disjoint_def, mem_span_singleton],
1003 rintro xp y yp a rfl,
1004 by_cases a0 : a = 0, {simp [a0]},
id ┴
typ ┴
st └┘
1005 exact xp.elim ((smul_mem_iff p a0).1 yp),
1006 end⟩
st └─┘
1007
1008 lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V)) (hx : x ∉ span K s) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1009 linear_independent K (λ b, b : insert x s → V) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1010 begin
1011 rw ← union_singleton,
1012 have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
id ┴
typ ┴
1013 apply linear_independent_union hs (linear_independent_singleton x0),
1014 rwa [disjoint_span_singleton x0]
1015 end
st └─┘
1016
1017 lemma exists_linear_independent (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ t) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1018 ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (λ x, x : b → V) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1019 begin
1020 rcases zorn.zorn_subset₀ {b | b ⊆ t ∧ linear_independent K (λ x, x : b → V)} _ _
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1021 ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
1022 { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
id ┴ ┴
typ ┴ ┴
1023 haveI := classical.dec (x ∈ span K b),
id └───────────┘ ┴ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴ ┴
1024 by_contra hn,
1025 apply hn,
1026 rw ← h _ ⟨insert_subset.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _),
1027 exact subset_span (mem_insert _ _) },
st └┘
1028 { refine λ c hc cc c0, ⟨⋃₀ c, ⟨_, _⟩, λ x, _⟩,
id ┴ └┘ ┴
typ ┴ └┘ ┴
1029 { exact sUnion_subset (λ x xc, (hc xc).1) },
id ┴
typ ┴
st └┘
1030 { exact linear_independent_sUnion_of_directed cc.directed_on (λ x xc, (hc xc).2) },
id ┴
typ ┴
st └┘
1031 { exact subset_sUnion_of_mem } }
st └───
1032 end
st ──┘
1033
1034 lemma exists_subset_is_basis (hs : linear_independent K (λ x, x : s → V)) :
id ┴ ┴
typ ┴ ┴
1035 ∃b, s ⊆ b ∧ is_basis K (λ i : b, i.val) :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
1036 let ⟨b, hb₀, hx, hb₂, hb₃⟩ := exists_linear_independent hs (@subset_univ _ _) in
id ┴
typ ┴
1037 ⟨ b, hx,
1038 @linear_independent.restrict_of_comp_subtype _ _ _ id _ _ _ _ hb₃,
1039 by simp; exact eq_top_iff.2 hb₂⟩
1040
1041 variables (K V)
1042 lemma exists_is_basis : ∃b : set V, is_basis K (λ i : b, i.val) :=
id ┴ ┴
typ ┴ ┴
1043 let ⟨b, _, hb⟩ := exists_subset_is_basis linear_independent_empty in ⟨b, hb⟩
id ┴
typ ┴
1044
1045 variables {K V}
1046
1047 -- TODO(Mario): rewrite?
1048 lemma exists_of_linear_independent_of_finite_span {t : finset V}
id └┘ ┴
src └┘
typ └┘ ┴
doc └┘
1049 (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ (span K ↑t : submodule K V)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1050 ∃t':finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card :=
id ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
src ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴
1051 have ∀t, ∀(s' : finset V), ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ (span K ↑(s' ∪ t) : submodule K V) →
id ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
1052 ∃t':finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
1053 assume t, finset.induction_on t
id ┴ ┴
typ ┴ ┴
1054 (assume s' hs' _ hss',
id └┘
typ └┘
1055 have s = ↑s',
id ┴ └┘
typ ┴ └┘
1056 from eq_of_linear_independent_of_span_subtype (@zero_ne_one K _) hs hs' $
id ┴
typ ┴
1057 by simpa using hss',
1058 ⟨s', by simp [this]⟩)
id └┘
typ └┘
1059 (assume b₁ t hb₁t ih s' hs' hst hss',
id └┘ ┴ └┘
typ └┘ ┴ └┘
1060 have hb₁s : b₁ ∉ s,
id └┘ ┴
typ └┘ ┴
1061 from assume h,
1062 have b₁ ∈ s ∩ ↑(insert b₁ t), from ⟨h, finset.mem_insert_self _ _⟩,
id └┘ ┴ └┘ ┴
typ └┘ ┴ └┘ ┴
1063 by rwa [hst] at this,
1064 have hb₁s' : b₁ ∉ s', from assume h, hb₁s $ hs' h,
id └┘ └┘
typ └┘ └┘
1065 have hst : s ∩ ↑t = ∅,
id ┴ ┴
typ ┴ ┴
1066 from eq_empty_of_subset_empty $ subset.trans
1067 (by simp [inter_subset_inter, subset.refl]) (le_of_eq hst),
1068 classical.by_cases
1069 (assume : s ⊆ (span K ↑(s' ∪ t) : submodule K V),
id ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
1070 let ⟨u, hust, hsu, eq⟩ := ih _ hs' hst this in
id ┴
typ ┴
1071 have hb₁u : b₁ ∉ u, from assume h, (hust h).elim hb₁s hb₁t,
id └┘
typ └┘
1072 ⟨insert b₁ u, by simp [insert_subset_insert hust],
id └┘
typ └┘
1073 subset.trans hsu (by simp), by simp [eq, hb₁t, hb₁s', hb₁u]⟩)
1074 (assume : ¬ s ⊆ (span K ↑(s' ∪ t) : submodule K V),
id ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
1075 let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this in
id └┘
typ └┘
1076 have hb₂t' : b₂ ∉ s' ∪ t, from assume h, hb₂t $ subset_span h,
id └┘ ┴
typ └┘ ┴
1077 have s ⊆ (span K ↑(insert b₂ s' ∪ t) : submodule K V), from
id ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
1078 assume b₃ hb₃,
id └┘
typ └┘
1079 have ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : set V),
id └┘ └┘ ┴ └┘ └┘ ┴ └─┘ ┴
src └─┘
typ └┘ └┘ ┴ └┘ └┘ ┴ └─┘ ┴
1080 by simp [insert_eq, -singleton_union, -union_singleton, union_subset_union, subset.refl, subset_union_right],
1081 have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : set V)),
id └┘ ┴ └┘ └┘ ┴ └─┘ ┴
src └─┘
typ └┘ ┴ └┘ └┘ ┴ └─┘ ┴
1082 from span_mono this (hss' hb₃),
1083 have s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : submodule K V),
id ┴ ┴ └┘ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴ ┴
1084 by simpa [insert_eq, -singleton_union, -union_singleton] using hss',
1085 have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)),
id └┘ ┴ └┘ ┴
typ └┘ ┴ └┘ ┴
1086 from mem_span_insert_exchange (this hb₂s) hb₂t,
1087 by rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃,
1088 let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset, hb₂s, hs']) hst this in
id ┴
typ ┴
1089 ⟨u, subset.trans hust $ union_subset_union (subset.refl _) (by simp [subset_insert]),
1090 hsu, by rw [finset.union_comm] at hb₂t'; simp [eq, hb₂t', hb₁t, hb₁s']⟩)),
1091 begin
1092 letI := classical.dec_pred (λx, x ∈ s),
id ┴ ┴
typ ┴ ┴
1093 have eq : t.filter (λx, x ∈ s) ∪ t.filter (λx, x ∉ s) = t,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1094 { apply finset.ext.mpr,
1095 intro x,
1096 by_cases x ∈ s; simp *, finish },
id ┴ ┴
typ ┴ ┴
st └┘
1097 apply exists.elim (this (t.filter (λx, x ∉ s)) (t.filter (λx, x ∈ s))
id ┴ ┴ ┴
typ ┴ ┴ ┴
1098 (by simp [set.subset_def]) (by simp [set.ext_iff] {contextual := tt}) (by rwa [eq])),
id └┘
src └┘
typ └┘
1099 intros u h,
1100 exact ⟨u, subset.trans h.1 (by simp [subset_def, and_imp, or_imp_distrib] {contextual:=tt}),
id ┴ └┘
src └┘
typ ┴ └┘
1101 h.2.1, by simp only [h.2.2, eq]⟩
1102 end
st └─┘
1103
1104 lemma exists_finite_card_le_of_finite_of_linear_independent_of_span
1105 (ht : finite t) (hs : linear_independent K (λ x, x : s → V)) (hst : s ⊆ span K t) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1106 ∃h : finite s, h.to_finset.card ≤ ht.to_finset.card :=
id ┴ ┴ └┘
typ ┴ ┴ └┘
1107 have s ⊆ (span K ↑(ht.to_finset) : submodule K V), by simp; assumption,
id ┴ ┴ ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ ┴ ┴ └────────┘
doc └────────┘
1108 let ⟨u, hust, hsu, eq⟩ := exists_of_linear_independent_of_finite_span hs this in
id ┴
typ ┴
1109 have finite s, from finite_subset u.finite_to_set hsu,
id ┴
typ ┴
1110 ⟨this, by rw [←eq]; exact (finset.card_le_of_subset $ finset.coe_subset.mp $ by simp [hsu])⟩
id └──┘
typ └──┘
1111
1112 lemma exists_left_inverse_linear_map_of_injective {f : V →ₗ[K] V'}
id ┴ ┴ └┘
typ ┴ ┴ └┘
1113 (hf_inj : f.ker = ⊥) : ∃g:V' →ₗ V, g.comp f = linear_map.id :=
id └┘ ┴
typ └┘ ┴
1114 begin
1115 rcases exists_is_basis K V with ⟨B, hB⟩,
id ┴ ┴
typ ┴ ┴
1116 have hB₀ : _ := hB.1.to_subtype_range,
1117 have : linear_independent K (λ x, x : f '' B → V'),
id ┴ ┴ └┘
typ ┴ ┴ └┘
1118 { have h₁ := hB₀.image_subtype (show disjoint (span K (range (λ i : B, i.val))) (linear_map.ker f), by simp [hf_inj]),
id ┴
typ ┴
1119 have h₂ : range (λ (i : B), i.val) = B := subtype.range_val B,
id ┴
typ ┴
1120 rwa h₂ at h₁ },
st └┘
1121 rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
1122 haveI : inhabited V := ⟨0⟩,
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
1123 use hC.constr (function.restrict (inv_fun f) C : C → V),
id ┴
typ ┴
1124 apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hB,
1125 intros b,
1126 rw image_subset_iff at BC,
1127 simp,
1128 have := BC (subtype.mem b),
1129 rw mem_preimage at this,
1130 have : f (b.val) = (subtype.mk (f ↑b) (begin rw ←mem_preimage, exact BC (subtype.mem b) end) : C).val,
id ┴
typ ┴
st └─┘
1131 by simp; unfold_coes,
1132 rw this,
1133 rw [constr_basis hC],
1134 exact left_inverse_inv_fun (linear_map.ker_eq_bot.1 hf_inj) _,
1135 end
st └─┘
1136
1137 lemma exists_right_inverse_linear_map_of_surjective {f : V →ₗ[K] V'}
id ┴ ┴ └┘
typ ┴ ┴ └┘
1138 (hf_surj : f.range = ⊤) : ∃g:V' →ₗ V, f.comp g = linear_map.id :=
id └┘ ┴
typ └┘ ┴
1139 begin
1140 rcases exists_is_basis K V' with ⟨C, hC⟩,
id ┴ └┘
typ ┴ └┘
1141 haveI : inhabited V := ⟨0⟩,
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
1142 use hC.constr (function.restrict (inv_fun f) C : C → V),
id ┴
typ ┴
1143 apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hC,
1144 intros c,
1145 simp [constr_basis hC],
1146 exact right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) _
1147 end
st └─┘
1148
1149 set_option class.instance_max_depth 49
doc └──────────────────────┘
1150 open submodule linear_map
1151 theorem quotient_prod_linear_equiv (p : submodule K V) :
id ┴ ┴
typ ┴ ┴
1152 nonempty ((p.quotient × p) ≃ₗ[K] V) :=
id └┘ └┘ ┴ ┴ ┴
src └┘ └┘ ┴
typ └┘ └┘ ┴ ┴ ┴
1153 begin
1154 haveI := classical.dec_eq (quotient p),
1155 rcases exists_right_inverse_linear_map_of_surjective p.range_mkq with ⟨f, hf⟩,
1156 have mkf : ∀ x, submodule.quotient.mk (f x) = x := linear_map.ext_iff.1 hf,
1157 have fp : ∀ x, x - f (p.mkq x) ∈ p :=
id ┴
typ ┴
1158 λ x, (submodule.quotient.eq p).1 (mkf (p.mkq x)).symm,
id ┴
typ ┴
1159 refine ⟨linear_equiv.of_linear (f.copair p.subtype)
1160 (p.mkq.pair (cod_restrict p (linear_map.id - f.comp p.mkq) fp))
1161 (by ext; simp) _⟩,
1162 ext ⟨⟨x⟩, y, hy⟩; simp,
1163 { apply (submodule.quotient.eq p).2,
1164 simpa using sub_mem p hy (fp x) },
id ┴
typ ┴
st └┘
1165 { refine subtype.coe_ext.2 _,
1166 simp [mkf, (submodule.quotient.mk_eq_zero p).2 hy] }
st └─
1167 end
st ──┘
1168
1169 open fintype
1170
1171 theorem vector_space.card_fintype [fintype K] [fintype V] :
id └┘ └─┘ ┴ └┘ └┘ ┴
src └┘ └─┘ └┘ └┘
typ └┘ └─┘ ┴ └┘ └┘ ┴
doc └┘ └─┘ └┘ └┘
1172 ∃ n : ℕ, card V = (card K) ^ n :=
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
1173 begin
1174 apply exists.elim (exists_is_basis K V),
1175 intros b hb,
1176 haveI := classical.dec_pred (λ x, x ∈ b),
id ┴ ┴
typ ┴ ┴
1177 use card b,
id ┴
typ ┴
1178 exact module.card_fintype hb,
1179 end
st └─┘
1180
1181 end vector_space
1182
1183 namespace pi
1184 open set linear_map
1185
1186 section module
1187 variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
id ┴
typ ┴
1188 variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)] [fintype η]
id └┘ ┴ ┴ ┴ └─────┘
src └┘ └─────┘
typ └┘ ┴ ┴ ┴ └─────┘
doc └─────┘
1189
1190 lemma linear_independent_std_basis
1191 (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
1192 linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1193 begin
1194 have hs' : ∀j : η, linear_independent R (λ i : ιs j, std_basis R Ms j (v j i)),
id ┴ ┴ └┘
typ ┴ ┴ └┘
1195 { intro j,
1196 apply linear_independent.image (hs j),
id ┴
typ ┴
1197 simp [ker_std_basis] },
st └┘
1198 apply linear_independent_Union_finite hs',
1199 { assume j J _ hiJ,
1200 simp [(set.Union.equations._eqn_1 _).symm, submodule.span_image, submodule.span_Union],
1201 have h₀ : ∀ j, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
id ┴ └┘
typ ┴ └┘
1202 ≤ range (std_basis R Ms j),
id ┴ └┘
typ ┴ └┘
1203 { intro j,
1204 rw [span_le, linear_map.range_coe],
1205 apply range_comp_subset_range },
st └┘
1206 have h₁ : span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))
id └┘
typ └┘
1207 ≤ ⨆ i ∈ {j}, range (std_basis R Ms i),
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
1208 { rw @supr_singleton _ _ _ (λ i, linear_map.range (std_basis R (λ (j : η), Ms j) i)),
id ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘
1209 apply h₀ },
st └┘
1210 have h₂ : (⨆ j ∈ J, span R (range (λ (i : ιs j), std_basis R Ms j (v j i)))) ≤
id ┴ └┘
typ ┴ └┘
1211 ⨆ j ∈ J, range (std_basis R (λ (j : η), Ms j) j) :=
id ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
1212 supr_le_supr (λ i, supr_le_supr (λ H, h₀ i)),
id ┴
typ ┴
1213 have h₃ : disjoint (λ (i : η), i ∈ {j}) J,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1214 { convert set.disjoint_singleton_left.2 hiJ,
1215 rw ←@set_of_mem_eq _ {j},
id ┴
typ ┴
1216 refl },
st └┘
1217 refine disjoint_mono h₁ h₂
1218 (disjoint_std_basis_std_basis _ _ _ _ h₃), }
st └─
1219 end
st ──┘
1220
1221 lemma is_basis_std_basis (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
id ┴ └┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴
1222 is_basis R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (s ji.1 ji.2)) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1223 begin
1224 split,
1225 { apply linear_independent_std_basis _ (assume i, (hs i).1) },
st └┘
1226 have h₁ : Union (λ j, set.range (std_basis R Ms j ∘ s j))
id ┴
typ ┴
1227 ⊆ range (λ (ji : Σ (j : η), ιs j), (std_basis R Ms (ji.fst)) (s (ji.fst) (ji.snd))),
id ┴ └┘ ┴ └┘
typ ┴ └┘ ┴ └┘
1228 { apply Union_subset, intro i,
1229 apply range_comp_subset_range (λ x : ιs i, (⟨i, x⟩ : Σ (j : η), ιs j))
id ┴
typ ┴
1230 (λ (ji : Σ (j : η), ιs j), std_basis R Ms (ji.fst) (s (ji.fst) (ji.snd))) },
id ┴ ┴ └┘
typ ┴ ┴ └┘
st └┘
1231 have h₂ : ∀ i, span R (range (std_basis R Ms i ∘ s i)) = range (std_basis R Ms i),
id ┴ ┴ └┘
typ ┴ ┴ └┘
1232 { intro i,
1233 rw [set.range_comp, submodule.span_image, (assume i, (hs i).2), submodule.map_top] },
id ┴
typ ┴
st ┴ └┘
1234 apply eq_top_mono,
1235 apply span_mono h₁,
1236 rw span_Union,
1237 simp only [h₂],
1238 apply supr_range_std_basis
1239 end
st └─┘
1240
1241 section
1242 variables (R η)
1243
1244 lemma is_basis_fun₀ : is_basis R
id ┴
typ ┴
1245 (λ (ji : Σ (j : η), (λ _, unit) j),
id ┴ ┴ └──┘ ┴
src └──┘
typ ┴ ┴ └──┘ ┴
doc └──┘
1246 (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1247 begin
1248 haveI := classical.dec_eq,
1249 apply @is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ (λ _ _, (1 : R))
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
1250 (assume i, @is_basis_singleton_one _ _ _ _),
id ┴
typ ┴
1251 end
st └─┘
1252
1253 lemma is_basis_fun : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1254 begin
1255 apply is_basis.comp (is_basis_fun₀ R η) (λ i, ⟨i, punit.star⟩),
1256 apply bijective_iff_has_inverse.2,
1257 use (λ x, x.1),
1258 simp [function.left_inverse, function.right_inverse],
1259 intros _ b,
1260 rw [unique.eq_default b, unique.eq_default punit.star]
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
st ┴
1261 end
st └─┘
1262
1263 end
1264
1265 end module
1266
1267 end pi